isopos - Mathbox for Norm Megill

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

Theorem isopos 32791

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 5888	. . . . . . 7
2		isopos.b	. . . . . . 7
3	1, 2	syl6eqr 2514	. . . . . 6
4		fveq2 5888	. . . . . . . 8
5		isopos.e	. . . . . . . 8
6	4, 5	syl6eqr 2514	. . . . . . 7
7	6	dmeqd 5056	. . . . . 6
8	3, 7	eleq12d 2534	. . . . 5
9		fveq2 5888	. . . . . . . 8
10		isopos.g	. . . . . . . 8
11	9, 10	syl6eqr 2514	. . . . . . 7
12	11	dmeqd 5056	. . . . . 6
13	3, 12	eleq12d 2534	. . . . 5
14	8, 13	anbi12d 722	. . . 4 $/\$ $/\$
15		fveq2 5888	. . . . . . . 8
16		isopos.o	. . . . . . . 8
17	15, 16	syl6eqr 2514	. . . . . . 7
18	17	eqeq2d 2472	. . . . . 6
19	3	eleq2d 2525	. . . . . . . . . 10
20		fveq2 5888	. . . . . . . . . . . . 13
21		isopos.l	. . . . . . . . . . . . 13
22	20, 21	syl6eqr 2514	. . . . . . . . . . . 12
23	22	breqd 4427	. . . . . . . . . . 11
24	22	breqd 4427	. . . . . . . . . . 11
25	23, 24	imbi12d 326	. . . . . . . . . 10
26	19, 25	3anbi13d 1350	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
27		fveq2 5888	. . . . . . . . . . . 12
28		isopos.j	. . . . . . . . . . . 12 $.\/$
29	27, 28	syl6eqr 2514	. . . . . . . . . . 11 $.\/$
30	29	oveqd 6332	. . . . . . . . . 10 $.\/$
31		fveq2 5888	. . . . . . . . . . 11
32		isopos.u	. . . . . . . . . . 11
33	31, 32	syl6eqr 2514	. . . . . . . . . 10
34	30, 33	eqeq12d 2477	. . . . . . . . 9 $.\/$
35		fveq2 5888	. . . . . . . . . . . 12
36		isopos.m	. . . . . . . . . . . 12 $./\$
37	35, 36	syl6eqr 2514	. . . . . . . . . . 11 $./\$
38	37	oveqd 6332	. . . . . . . . . 10 $./\$
39		fveq2 5888	. . . . . . . . . . 11
40		isopos.f	. . . . . . . . . . 11
41	39, 40	syl6eqr 2514	. . . . . . . . . 10
42	38, 41	eqeq12d 2477	. . . . . . . . 9 $./\$
43	26, 34, 42	3anbi123d 1348	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
44	3, 43	raleqbidv 3013	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
45	3, 44	raleqbidv 3013	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
46	18, 45	anbi12d 722	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
47	46	exbidv 1779	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
48	14, 47	anbi12d 722	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
49		df-oposet 32787	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	48, 49	elrab2 3210	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
51		anass 659	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
52		3anass 995	. . . 4 $/\$ $/\$ $/\$ $/\$
53	52	bicomi 207	. . 3 $/\$ $/\$ $/\$ $/\$
54		fvex 5898	. . . . 5
55	16, 54	eqeltri 2536	. . . 4
56		fveq1 5887	. . . . . . . 8
57	56	eleq1d 2524	. . . . . . 7
58		id 22	. . . . . . . . 9
59	58, 56	fveq12d 5894	. . . . . . . 8
60	59	eqeq1d 2464	. . . . . . 7
61		fveq1 5887	. . . . . . . . 9
62	61, 56	breq12d 4429	. . . . . . . 8
63	62	imbi2d 322	. . . . . . 7
64	57, 60, 63	3anbi123d 1348	. . . . . 6 $/\$ $/\$ $/\$ $/\$
65	56	oveq2d 6331	. . . . . . 7 $.\/$ $.\/$
66	65	eqeq1d 2464	. . . . . 6 $.\/$ $.\/$
67	56	oveq2d 6331	. . . . . . 7 $./\$ $./\$
68	67	eqeq1d 2464	. . . . . 6 $./\$ $./\$
69	64, 66, 68	3anbi123d 1348	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
70	69	2ralbidv 2844	. . . 4 $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
71	55, 70	ceqsexv 3096	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
72	53, 71	anbi12i 708	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$
73	50, 51, 72	3bitr2i 281	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $./\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 375 $/\$ w3a 991

wceq 1455

wex 1674

wcel 1898

wral 2749

cvv 3057 class class class wbr 4416

cdm 4853

cfv 5601 (class class class)co 6315

cbs 15170

cple 15246

coc 15247

cpo 16234

club 16236

cglb 16237

cjn 16238

cmee 16239

cp0 16332

cp1 16333

cops 32783

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-nul 4548

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-ral 2754 df-rex 2755 df-rab 2758 df-v 3059 df-sbc 3280 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-br 4417 df-dm 4863 df-iota 5565 df-fv 5609 df-ov 6318 df-oposet 32787

This theorem is referenced by: opposet 32792 oposlem 32793 op01dm 32794

W3C validator