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 33995

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 5866	. . . . . . 7
2		isopos.b	. . . . . . 7
3	1, 2	syl6eqr 2526	. . . . . 6
4		fveq2 5866	. . . . . . . 8
5		isopos.e	. . . . . . . 8
6	4, 5	syl6eqr 2526	. . . . . . 7
7	6	dmeqd 5205	. . . . . 6
8	3, 7	eleq12d 2549	. . . . 5
9		fveq2 5866	. . . . . . . 8
10		isopos.g	. . . . . . . 8
11	9, 10	syl6eqr 2526	. . . . . . 7
12	11	dmeqd 5205	. . . . . 6
13	3, 12	eleq12d 2549	. . . . 5
14	8, 13	anbi12d 710	. . . 4 $/\$ $/\$
15		fveq2 5866	. . . . . . . 8
16		isopos.o	. . . . . . . 8
17	15, 16	syl6eqr 2526	. . . . . . 7
18	17	eqeq2d 2481	. . . . . 6
19	3	eleq2d 2537	. . . . . . . . . 10
20		fveq2 5866	. . . . . . . . . . . . 13
21		isopos.l	. . . . . . . . . . . . 13
22	20, 21	syl6eqr 2526	. . . . . . . . . . . 12
23	22	breqd 4458	. . . . . . . . . . 11
24	22	breqd 4458	. . . . . . . . . . 11
25	23, 24	imbi12d 320	. . . . . . . . . 10
26	19, 25	3anbi13d 1301	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
27		fveq2 5866	. . . . . . . . . . . 12
28		isopos.j	. . . . . . . . . . . 12 $.\/$
29	27, 28	syl6eqr 2526	. . . . . . . . . . 11 $.\/$
30	29	oveqd 6301	. . . . . . . . . 10 $.\/$
31		fveq2 5866	. . . . . . . . . . 11
32		isopos.u	. . . . . . . . . . 11
33	31, 32	syl6eqr 2526	. . . . . . . . . 10
34	30, 33	eqeq12d 2489	. . . . . . . . 9 $.\/$
35		fveq2 5866	. . . . . . . . . . . 12
36		isopos.m	. . . . . . . . . . . 12 $./\$
37	35, 36	syl6eqr 2526	. . . . . . . . . . 11 $./\$
38	37	oveqd 6301	. . . . . . . . . 10 $./\$
39		fveq2 5866	. . . . . . . . . . 11
40		isopos.f	. . . . . . . . . . 11
41	39, 40	syl6eqr 2526	. . . . . . . . . 10
42	38, 41	eqeq12d 2489	. . . . . . . . 9 $./\$
43	26, 34, 42	3anbi123d 1299	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
44	3, 43	raleqbidv 3072	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
45	3, 44	raleqbidv 3072	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
46	18, 45	anbi12d 710	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
47	46	exbidv 1690	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
48	14, 47	anbi12d 710	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
49		df-oposet 33991	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	48, 49	elrab2 3263	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
51		anass 649	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
52		3anass 977	. . . 4 $/\$ $/\$ $/\$ $/\$
53	52	bicomi 202	. . 3 $/\$ $/\$ $/\$ $/\$
54		fvex 5876	. . . . 5
55	16, 54	eqeltri 2551	. . . 4
56		fveq1 5865	. . . . . . . 8
57	56	eleq1d 2536	. . . . . . 7
58		id 22	. . . . . . . . 9
59	58, 56	fveq12d 5872	. . . . . . . 8
60	59	eqeq1d 2469	. . . . . . 7
61		fveq1 5865	. . . . . . . . 9
62	61, 56	breq12d 4460	. . . . . . . 8
63	62	imbi2d 316	. . . . . . 7
64	57, 60, 63	3anbi123d 1299	. . . . . 6 $/\$ $/\$ $/\$ $/\$
65	56	oveq2d 6300	. . . . . . 7 $.\/$ $.\/$
66	65	eqeq1d 2469	. . . . . 6 $.\/$ $.\/$
67	56	oveq2d 6300	. . . . . . 7 $./\$ $./\$
68	67	eqeq1d 2469	. . . . . 6 $./\$ $./\$
69	64, 66, 68	3anbi123d 1299	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
70	69	2ralbidv 2908	. . . 4 $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
71	55, 70	ceqsexv 3150	. . 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 1379

wex 1596

wcel 1767

wral 2814

cvv 3113 class class class wbr 4447

cdm 4999

cfv 5588 (class class class)co 6284

cbs 14490

cple 14562

coc 14563

cpo 15427

club 15429

cglb 15430

cjn 15431

cmee 15432

cp0 15524

cp1 15525

cops 33987

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-nul 4576

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-rab 2823 df-v 3115 df-sbc 3332 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-nul 3786 df-if 3940 df-sn 4028 df-pr 4030 df-op 4034 df-uni 4246 df-br 4448 df-dm 5009 df-iota 5551 df-fv 5596 df-ov 6287 df-oposet 33991

This theorem is referenced by: opposet 33996 oposlem 33997 op01dm 33998

W3C validator