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 32513

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 5688	. . . . . . 7
2		isopos.b	. . . . . . 7
3	1, 2	syl6eqr 2491	. . . . . 6
4		fveq2 5688	. . . . . . . 8
5		isopos.e	. . . . . . . 8
6	4, 5	syl6eqr 2491	. . . . . . 7
7	6	dmeqd 5038	. . . . . 6
8	3, 7	eleq12d 2509	. . . . 5
9		fveq2 5688	. . . . . . . 8
10		isopos.g	. . . . . . . 8
11	9, 10	syl6eqr 2491	. . . . . . 7
12	11	dmeqd 5038	. . . . . 6
13	3, 12	eleq12d 2509	. . . . 5
14	8, 13	anbi12d 705	. . . 4 $/\$ $/\$
15		fveq2 5688	. . . . . . . 8
16		isopos.o	. . . . . . . 8
17	15, 16	syl6eqr 2491	. . . . . . 7
18	17	eqeq2d 2452	. . . . . 6
19	3	eleq2d 2508	. . . . . . . . . 10
20		fveq2 5688	. . . . . . . . . . . . 13
21		isopos.l	. . . . . . . . . . . . 13
22	20, 21	syl6eqr 2491	. . . . . . . . . . . 12
23	22	breqd 4300	. . . . . . . . . . 11
24	22	breqd 4300	. . . . . . . . . . 11
25	23, 24	imbi12d 320	. . . . . . . . . 10
26	19, 25	3anbi13d 1286	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
27		fveq2 5688	. . . . . . . . . . . 12
28		isopos.j	. . . . . . . . . . . 12 $.\/$
29	27, 28	syl6eqr 2491	. . . . . . . . . . 11 $.\/$
30	29	oveqd 6107	. . . . . . . . . 10 $.\/$
31		fveq2 5688	. . . . . . . . . . 11
32		isopos.u	. . . . . . . . . . 11
33	31, 32	syl6eqr 2491	. . . . . . . . . 10
34	30, 33	eqeq12d 2455	. . . . . . . . 9 $.\/$
35		fveq2 5688	. . . . . . . . . . . 12
36		isopos.m	. . . . . . . . . . . 12 $./\$
37	35, 36	syl6eqr 2491	. . . . . . . . . . 11 $./\$
38	37	oveqd 6107	. . . . . . . . . 10 $./\$
39		fveq2 5688	. . . . . . . . . . 11
40		isopos.f	. . . . . . . . . . 11
41	39, 40	syl6eqr 2491	. . . . . . . . . 10
42	38, 41	eqeq12d 2455	. . . . . . . . 9 $./\$
43	26, 34, 42	3anbi123d 1284	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
44	3, 43	raleqbidv 2929	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
45	3, 44	raleqbidv 2929	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
46	18, 45	anbi12d 705	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
47	46	exbidv 1685	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
48	14, 47	anbi12d 705	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
49		df-oposet 32509	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	48, 49	elrab2 3116	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
51		anass 644	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
52		3anass 964	. . . 4 $/\$ $/\$ $/\$ $/\$
53	52	bicomi 202	. . 3 $/\$ $/\$ $/\$ $/\$
54		fvex 5698	. . . . 5
55	16, 54	eqeltri 2511	. . . 4
56		fveq1 5687	. . . . . . . 8
57	56	eleq1d 2507	. . . . . . 7
58		id 22	. . . . . . . . 9
59	58, 56	fveq12d 5694	. . . . . . . 8
60	59	eqeq1d 2449	. . . . . . 7
61		fveq1 5687	. . . . . . . . 9
62	61, 56	breq12d 4302	. . . . . . . 8
63	62	imbi2d 316	. . . . . . 7
64	57, 60, 63	3anbi123d 1284	. . . . . 6 $/\$ $/\$ $/\$ $/\$
65	56	oveq2d 6106	. . . . . . 7 $.\/$ $.\/$
66	65	eqeq1d 2449	. . . . . 6 $.\/$ $.\/$
67	56	oveq2d 6106	. . . . . . 7 $./\$ $./\$
68	67	eqeq1d 2449	. . . . . 6 $./\$ $./\$
69	64, 66, 68	3anbi123d 1284	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
70	69	2ralbidv 2755	. . . 4 $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
71	55, 70	ceqsexv 3006	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
72	53, 71	anbi12i 692	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
73	50, 51, 72	3bitr2i 273	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1364

wex 1591

wcel 1761

wral 2713

cvv 2970 class class class wbr 4289

cdm 4836

cfv 5415 (class class class)co 6090

cbs 14170

cple 14241

coc 14242

cpo 15106

club 15108

cglb 15109

cjn 15110

cmee 15111

cp0 15203

cp1 15204

cops 32505

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-nul 4418

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2263 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-ral 2718 df-rex 2719 df-rab 2722 df-v 2972 df-sbc 3184 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-nul 3635 df-if 3789 df-sn 3875 df-pr 3877 df-op 3881 df-uni 4089 df-br 4290 df-dm 4846 df-iota 5378 df-fv 5423 df-ov 6093 df-oposet 32509

This theorem is referenced by: opposet 32514 oposlem 32515 op01dm 32516

W3C validator