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 32825

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 5691	. . . . . . 7
2		isopos.b	. . . . . . 7
3	1, 2	syl6eqr 2493	. . . . . 6
4		fveq2 5691	. . . . . . . 8
5		isopos.e	. . . . . . . 8
6	4, 5	syl6eqr 2493	. . . . . . 7
7	6	dmeqd 5042	. . . . . 6
8	3, 7	eleq12d 2511	. . . . 5
9		fveq2 5691	. . . . . . . 8
10		isopos.g	. . . . . . . 8
11	9, 10	syl6eqr 2493	. . . . . . 7
12	11	dmeqd 5042	. . . . . 6
13	3, 12	eleq12d 2511	. . . . 5
14	8, 13	anbi12d 710	. . . 4 $/\$ $/\$
15		fveq2 5691	. . . . . . . 8
16		isopos.o	. . . . . . . 8
17	15, 16	syl6eqr 2493	. . . . . . 7
18	17	eqeq2d 2454	. . . . . 6
19	3	eleq2d 2510	. . . . . . . . . 10
20		fveq2 5691	. . . . . . . . . . . . 13
21		isopos.l	. . . . . . . . . . . . 13
22	20, 21	syl6eqr 2493	. . . . . . . . . . . 12
23	22	breqd 4303	. . . . . . . . . . 11
24	22	breqd 4303	. . . . . . . . . . 11
25	23, 24	imbi12d 320	. . . . . . . . . 10
26	19, 25	3anbi13d 1291	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
27		fveq2 5691	. . . . . . . . . . . 12
28		isopos.j	. . . . . . . . . . . 12 $.\/$
29	27, 28	syl6eqr 2493	. . . . . . . . . . 11 $.\/$
30	29	oveqd 6108	. . . . . . . . . 10 $.\/$
31		fveq2 5691	. . . . . . . . . . 11
32		isopos.u	. . . . . . . . . . 11
33	31, 32	syl6eqr 2493	. . . . . . . . . 10
34	30, 33	eqeq12d 2457	. . . . . . . . 9 $.\/$
35		fveq2 5691	. . . . . . . . . . . 12
36		isopos.m	. . . . . . . . . . . 12 $./\$
37	35, 36	syl6eqr 2493	. . . . . . . . . . 11 $./\$
38	37	oveqd 6108	. . . . . . . . . 10 $./\$
39		fveq2 5691	. . . . . . . . . . 11
40		isopos.f	. . . . . . . . . . 11
41	39, 40	syl6eqr 2493	. . . . . . . . . 10
42	38, 41	eqeq12d 2457	. . . . . . . . 9 $./\$
43	26, 34, 42	3anbi123d 1289	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
44	3, 43	raleqbidv 2931	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
45	3, 44	raleqbidv 2931	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
46	18, 45	anbi12d 710	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
47	46	exbidv 1680	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
48	14, 47	anbi12d 710	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
49		df-oposet 32821	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	48, 49	elrab2 3119	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
51		anass 649	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
52		3anass 969	. . . 4 $/\$ $/\$ $/\$ $/\$
53	52	bicomi 202	. . 3 $/\$ $/\$ $/\$ $/\$
54		fvex 5701	. . . . 5
55	16, 54	eqeltri 2513	. . . 4
56		fveq1 5690	. . . . . . . 8
57	56	eleq1d 2509	. . . . . . 7
58		id 22	. . . . . . . . 9
59	58, 56	fveq12d 5697	. . . . . . . 8
60	59	eqeq1d 2451	. . . . . . 7
61		fveq1 5690	. . . . . . . . 9
62	61, 56	breq12d 4305	. . . . . . . 8
63	62	imbi2d 316	. . . . . . 7
64	57, 60, 63	3anbi123d 1289	. . . . . 6 $/\$ $/\$ $/\$ $/\$
65	56	oveq2d 6107	. . . . . . 7 $.\/$ $.\/$
66	65	eqeq1d 2451	. . . . . 6 $.\/$ $.\/$
67	56	oveq2d 6107	. . . . . . 7 $./\$ $./\$
68	67	eqeq1d 2451	. . . . . 6 $./\$ $./\$
69	64, 66, 68	3anbi123d 1289	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
70	69	2ralbidv 2757	. . . 4 $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
71	55, 70	ceqsexv 3009	. . 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 965

wceq 1369

wex 1586

wcel 1756

wral 2715

cvv 2972 class class class wbr 4292

cdm 4840

cfv 5418 (class class class)co 6091

cbs 14174

cple 14245

coc 14246

cpo 15110

club 15112

cglb 15113

cjn 15114

cmee 15115

cp0 15207

cp1 15208

cops 32817

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-nul 4421

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-ral 2720 df-rex 2721 df-rab 2724 df-v 2974 df-sbc 3187 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-nul 3638 df-if 3792 df-sn 3878 df-pr 3880 df-op 3884 df-uni 4092 df-br 4293 df-dm 4850 df-iota 5381 df-fv 5426 df-ov 6094 df-oposet 32821

This theorem is referenced by: opposet 32826 oposlem 32827 op01dm 32828

W3C validator