isopos - Mathbox for Norm Megill

	Mathbox for Norm Megill	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > isopos		Structured version Unicode version

Theorem isopos 35048

Description: The predicate "is an orthoposet." (Contributed by NM, 20-Oct-2011.) (Revised by NM, 14-Sep-2018.)

**Hypotheses**
Ref	Expression
isopos.b
isopos.e
isopos.g
isopos.l
isopos.o
isopos.j	$.\/$
isopos.m	$./\$
isopos.f
isopos.u

**Assertion**
Ref	Expression
isopos	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

) $.\/$ (

)

(

) $./\$ (

)

(

)

Proof of Theorem isopos Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5872	. . . . . . 7
2		isopos.b	. . . . . . 7
3	1, 2	syl6eqr 2516	. . . . . 6
4		fveq2 5872	. . . . . . . 8
5		isopos.e	. . . . . . . 8
6	4, 5	syl6eqr 2516	. . . . . . 7
7	6	dmeqd 5215	. . . . . 6
8	3, 7	eleq12d 2539	. . . . 5
9		fveq2 5872	. . . . . . . 8
10		isopos.g	. . . . . . . 8
11	9, 10	syl6eqr 2516	. . . . . . 7
12	11	dmeqd 5215	. . . . . 6
13	3, 12	eleq12d 2539	. . . . 5
14	8, 13	anbi12d 710	. . . 4 $/\$ $/\$
15		fveq2 5872	. . . . . . . 8
16		isopos.o	. . . . . . . 8
17	15, 16	syl6eqr 2516	. . . . . . 7
18	17	eqeq2d 2471	. . . . . 6
19	3	eleq2d 2527	. . . . . . . . . 10
20		fveq2 5872	. . . . . . . . . . . . 13
21		isopos.l	. . . . . . . . . . . . 13
22	20, 21	syl6eqr 2516	. . . . . . . . . . . 12
23	22	breqd 4467	. . . . . . . . . . 11
24	22	breqd 4467	. . . . . . . . . . 11
25	23, 24	imbi12d 320	. . . . . . . . . 10
26	19, 25	3anbi13d 1301	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
27		fveq2 5872	. . . . . . . . . . . 12
28		isopos.j	. . . . . . . . . . . 12 $.\/$
29	27, 28	syl6eqr 2516	. . . . . . . . . . 11 $.\/$
30	29	oveqd 6313	. . . . . . . . . 10 $.\/$
31		fveq2 5872	. . . . . . . . . . 11
32		isopos.u	. . . . . . . . . . 11
33	31, 32	syl6eqr 2516	. . . . . . . . . 10
34	30, 33	eqeq12d 2479	. . . . . . . . 9 $.\/$
35		fveq2 5872	. . . . . . . . . . . 12
36		isopos.m	. . . . . . . . . . . 12 $./\$
37	35, 36	syl6eqr 2516	. . . . . . . . . . 11 $./\$
38	37	oveqd 6313	. . . . . . . . . 10 $./\$
39		fveq2 5872	. . . . . . . . . . 11
40		isopos.f	. . . . . . . . . . 11
41	39, 40	syl6eqr 2516	. . . . . . . . . 10
42	38, 41	eqeq12d 2479	. . . . . . . . 9 $./\$
43	26, 34, 42	3anbi123d 1299	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
44	3, 43	raleqbidv 3068	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
45	3, 44	raleqbidv 3068	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
46	18, 45	anbi12d 710	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
47	46	exbidv 1715	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
48	14, 47	anbi12d 710	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
49		df-oposet 35044	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	48, 49	elrab2 3259	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
51		anass 649	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
52		3anass 977	. . . 4 $/\$ $/\$ $/\$ $/\$
53	52	bicomi 202	. . 3 $/\$ $/\$ $/\$ $/\$
54		fvex 5882	. . . . 5
55	16, 54	eqeltri 2541	. . . 4
56		fveq1 5871	. . . . . . . 8
57	56	eleq1d 2526	. . . . . . 7
58		id 22	. . . . . . . . 9
59	58, 56	fveq12d 5878	. . . . . . . 8
60	59	eqeq1d 2459	. . . . . . 7
61		fveq1 5871	. . . . . . . . 9
62	61, 56	breq12d 4469	. . . . . . . 8
63	62	imbi2d 316	. . . . . . 7
64	57, 60, 63	3anbi123d 1299	. . . . . 6 $/\$ $/\$ $/\$ $/\$
65	56	oveq2d 6312	. . . . . . 7 $.\/$ $.\/$
66	65	eqeq1d 2459	. . . . . 6 $.\/$ $.\/$
67	56	oveq2d 6312	. . . . . . 7 $./\$ $./\$
68	67	eqeq1d 2459	. . . . . 6 $./\$ $./\$
69	64, 66, 68	3anbi123d 1299	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
70	69	2ralbidv 2901	. . . 4 $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
71	55, 70	ceqsexv 3146	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
72	53, 71	anbi12i 697	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
73	50, 51, 72	3bitr2i 273	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 973

wceq 1395

wex 1613

wcel 1819

wral 2807

cvv 3109 class class class wbr 4456

cdm 5008

cfv 5594 (class class class)co 6296

cbs 14644

cple 14719

coc 14720

cpo 15696

club 15698

cglb 15699

cjn 15700

cmee 15701

cp0 15794

cp1 15795

cops 35040

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-nul 4586

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-ral 2812 df-rex 2813 df-rab 2816 df-v 3111 df-sbc 3328 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-nul 3794 df-if 3945 df-sn 4033 df-pr 4035 df-op 4039 df-uni 4252 df-br 4457 df-dm 5018 df-iota 5557 df-fv 5602 df-ov 6299 df-oposet 35044

This theorem is referenced by: opposet 35049 oposlem 35050 op01dm 35051

W3C validator