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

Theorem isopos 36756
 Description: The predicate "is an orthoposet." (Contributed by NM, 20-Oct-2011.) (Revised by NM, 14-Sep-2018.)
Hypotheses
Ref Expression
isopos.b 𝐵 = (Base‘𝐾)
isopos.e 𝑈 = (lub‘𝐾)
isopos.g 𝐺 = (glb‘𝐾)
isopos.l = (le‘𝐾)
isopos.o = (oc‘𝐾)
isopos.j = (join‘𝐾)
isopos.m = (meet‘𝐾)
isopos.f 0 = (0.‘𝐾)
isopos.u 1 = (1.‘𝐾)
Assertion
Ref Expression
isopos (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ∧ ∀𝑥𝐵𝑦𝐵 ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 )))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑥, ,𝑦   𝑥,𝐾,𝑦
Allowed substitution hints:   𝑈(𝑥,𝑦)   1 (𝑥,𝑦)   𝐺(𝑥,𝑦)   (𝑥,𝑦)   (𝑥,𝑦)   (𝑥,𝑦)   0 (𝑥,𝑦)

Proof of Theorem isopos
Dummy variables 𝑛 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6658 . . . . . . 7 (𝑝 = 𝐾 → (Base‘𝑝) = (Base‘𝐾))
2 isopos.b . . . . . . 7 𝐵 = (Base‘𝐾)
31, 2eqtr4di 2811 . . . . . 6 (𝑝 = 𝐾 → (Base‘𝑝) = 𝐵)
4 fveq2 6658 . . . . . . . 8 (𝑝 = 𝐾 → (lub‘𝑝) = (lub‘𝐾))
5 isopos.e . . . . . . . 8 𝑈 = (lub‘𝐾)
64, 5eqtr4di 2811 . . . . . . 7 (𝑝 = 𝐾 → (lub‘𝑝) = 𝑈)
76dmeqd 5745 . . . . . 6 (𝑝 = 𝐾 → dom (lub‘𝑝) = dom 𝑈)
83, 7eleq12d 2846 . . . . 5 (𝑝 = 𝐾 → ((Base‘𝑝) ∈ dom (lub‘𝑝) ↔ 𝐵 ∈ dom 𝑈))
9 fveq2 6658 . . . . . . . 8 (𝑝 = 𝐾 → (glb‘𝑝) = (glb‘𝐾))
10 isopos.g . . . . . . . 8 𝐺 = (glb‘𝐾)
119, 10eqtr4di 2811 . . . . . . 7 (𝑝 = 𝐾 → (glb‘𝑝) = 𝐺)
1211dmeqd 5745 . . . . . 6 (𝑝 = 𝐾 → dom (glb‘𝑝) = dom 𝐺)
133, 12eleq12d 2846 . . . . 5 (𝑝 = 𝐾 → ((Base‘𝑝) ∈ dom (glb‘𝑝) ↔ 𝐵 ∈ dom 𝐺))
148, 13anbi12d 633 . . . 4 (𝑝 = 𝐾 → (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ↔ (𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺)))
15 fveq2 6658 . . . . . . . 8 (𝑝 = 𝐾 → (oc‘𝑝) = (oc‘𝐾))
16 isopos.o . . . . . . . 8 = (oc‘𝐾)
1715, 16eqtr4di 2811 . . . . . . 7 (𝑝 = 𝐾 → (oc‘𝑝) = )
1817eqeq2d 2769 . . . . . 6 (𝑝 = 𝐾 → (𝑛 = (oc‘𝑝) ↔ 𝑛 = ))
193eleq2d 2837 . . . . . . . . . 10 (𝑝 = 𝐾 → ((𝑛𝑥) ∈ (Base‘𝑝) ↔ (𝑛𝑥) ∈ 𝐵))
20 fveq2 6658 . . . . . . . . . . . . 13 (𝑝 = 𝐾 → (le‘𝑝) = (le‘𝐾))
21 isopos.l . . . . . . . . . . . . 13 = (le‘𝐾)
2220, 21eqtr4di 2811 . . . . . . . . . . . 12 (𝑝 = 𝐾 → (le‘𝑝) = )
2322breqd 5043 . . . . . . . . . . 11 (𝑝 = 𝐾 → (𝑥(le‘𝑝)𝑦𝑥 𝑦))
2422breqd 5043 . . . . . . . . . . 11 (𝑝 = 𝐾 → ((𝑛𝑦)(le‘𝑝)(𝑛𝑥) ↔ (𝑛𝑦) (𝑛𝑥)))
2523, 24imbi12d 348 . . . . . . . . . 10 (𝑝 = 𝐾 → ((𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥)) ↔ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))))
2619, 253anbi13d 1435 . . . . . . . . 9 (𝑝 = 𝐾 → (((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ↔ ((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥)))))
27 fveq2 6658 . . . . . . . . . . . 12 (𝑝 = 𝐾 → (join‘𝑝) = (join‘𝐾))
28 isopos.j . . . . . . . . . . . 12 = (join‘𝐾)
2927, 28eqtr4di 2811 . . . . . . . . . . 11 (𝑝 = 𝐾 → (join‘𝑝) = )
3029oveqd 7167 . . . . . . . . . 10 (𝑝 = 𝐾 → (𝑥(join‘𝑝)(𝑛𝑥)) = (𝑥 (𝑛𝑥)))
31 fveq2 6658 . . . . . . . . . . 11 (𝑝 = 𝐾 → (1.‘𝑝) = (1.‘𝐾))
32 isopos.u . . . . . . . . . . 11 1 = (1.‘𝐾)
3331, 32eqtr4di 2811 . . . . . . . . . 10 (𝑝 = 𝐾 → (1.‘𝑝) = 1 )
3430, 33eqeq12d 2774 . . . . . . . . 9 (𝑝 = 𝐾 → ((𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ↔ (𝑥 (𝑛𝑥)) = 1 ))
35 fveq2 6658 . . . . . . . . . . . 12 (𝑝 = 𝐾 → (meet‘𝑝) = (meet‘𝐾))
36 isopos.m . . . . . . . . . . . 12 = (meet‘𝐾)
3735, 36eqtr4di 2811 . . . . . . . . . . 11 (𝑝 = 𝐾 → (meet‘𝑝) = )
3837oveqd 7167 . . . . . . . . . 10 (𝑝 = 𝐾 → (𝑥(meet‘𝑝)(𝑛𝑥)) = (𝑥 (𝑛𝑥)))
39 fveq2 6658 . . . . . . . . . . 11 (𝑝 = 𝐾 → (0.‘𝑝) = (0.‘𝐾))
40 isopos.f . . . . . . . . . . 11 0 = (0.‘𝐾)
4139, 40eqtr4di 2811 . . . . . . . . . 10 (𝑝 = 𝐾 → (0.‘𝑝) = 0 )
4238, 41eqeq12d 2774 . . . . . . . . 9 (𝑝 = 𝐾 → ((𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝) ↔ (𝑥 (𝑛𝑥)) = 0 ))
4326, 34, 423anbi123d 1433 . . . . . . . 8 (𝑝 = 𝐾 → ((((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ∧ (𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝)) ↔ (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 )))
443, 43raleqbidv 3319 . . . . . . 7 (𝑝 = 𝐾 → (∀𝑦 ∈ (Base‘𝑝)(((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ∧ (𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝)) ↔ ∀𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 )))
453, 44raleqbidv 3319 . . . . . 6 (𝑝 = 𝐾 → (∀𝑥 ∈ (Base‘𝑝)∀𝑦 ∈ (Base‘𝑝)(((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ∧ (𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝)) ↔ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 )))
4618, 45anbi12d 633 . . . . 5 (𝑝 = 𝐾 → ((𝑛 = (oc‘𝑝) ∧ ∀𝑥 ∈ (Base‘𝑝)∀𝑦 ∈ (Base‘𝑝)(((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ∧ (𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝))) ↔ (𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 ))))
4746exbidv 1922 . . . 4 (𝑝 = 𝐾 → (∃𝑛(𝑛 = (oc‘𝑝) ∧ ∀𝑥 ∈ (Base‘𝑝)∀𝑦 ∈ (Base‘𝑝)(((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ∧ (𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝))) ↔ ∃𝑛(𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 ))))
4814, 47anbi12d 633 . . 3 (𝑝 = 𝐾 → ((((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑛(𝑛 = (oc‘𝑝) ∧ ∀𝑥 ∈ (Base‘𝑝)∀𝑦 ∈ (Base‘𝑝)(((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ∧ (𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝)))) ↔ ((𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ∧ ∃𝑛(𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 )))))
49 df-oposet 36752 . . 3 OP = {𝑝 ∈ Poset ∣ (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑛(𝑛 = (oc‘𝑝) ∧ ∀𝑥 ∈ (Base‘𝑝)∀𝑦 ∈ (Base‘𝑝)(((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ∧ (𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝))))}
5048, 49elrab2 3605 . 2 (𝐾 ∈ OP ↔ (𝐾 ∈ Poset ∧ ((𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ∧ ∃𝑛(𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 )))))
51 anass 472 . 2 (((𝐾 ∈ Poset ∧ (𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺)) ∧ ∃𝑛(𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 ))) ↔ (𝐾 ∈ Poset ∧ ((𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ∧ ∃𝑛(𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 )))))
52 3anass 1092 . . . 4 ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ↔ (𝐾 ∈ Poset ∧ (𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺)))
5352bicomi 227 . . 3 ((𝐾 ∈ Poset ∧ (𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺)) ↔ (𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺))
5416fvexi 6672 . . . 4 ∈ V
55 fveq1 6657 . . . . . . . 8 (𝑛 = → (𝑛𝑥) = ( 𝑥))
5655eleq1d 2836 . . . . . . 7 (𝑛 = → ((𝑛𝑥) ∈ 𝐵 ↔ ( 𝑥) ∈ 𝐵))
57 id 22 . . . . . . . . 9 (𝑛 = 𝑛 = )
5857, 55fveq12d 6665 . . . . . . . 8 (𝑛 = → (𝑛‘(𝑛𝑥)) = ( ‘( 𝑥)))
5958eqeq1d 2760 . . . . . . 7 (𝑛 = → ((𝑛‘(𝑛𝑥)) = 𝑥 ↔ ( ‘( 𝑥)) = 𝑥))
60 fveq1 6657 . . . . . . . . 9 (𝑛 = → (𝑛𝑦) = ( 𝑦))
6160, 55breq12d 5045 . . . . . . . 8 (𝑛 = → ((𝑛𝑦) (𝑛𝑥) ↔ ( 𝑦) ( 𝑥)))
6261imbi2d 344 . . . . . . 7 (𝑛 = → ((𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥)) ↔ (𝑥 𝑦 → ( 𝑦) ( 𝑥))))
6356, 59, 623anbi123d 1433 . . . . . 6 (𝑛 = → (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ↔ (( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥)))))
6455oveq2d 7166 . . . . . . 7 (𝑛 = → (𝑥 (𝑛𝑥)) = (𝑥 ( 𝑥)))
6564eqeq1d 2760 . . . . . 6 (𝑛 = → ((𝑥 (𝑛𝑥)) = 1 ↔ (𝑥 ( 𝑥)) = 1 ))
6655oveq2d 7166 . . . . . . 7 (𝑛 = → (𝑥 (𝑛𝑥)) = (𝑥 ( 𝑥)))
6766eqeq1d 2760 . . . . . 6 (𝑛 = → ((𝑥 (𝑛𝑥)) = 0 ↔ (𝑥 ( 𝑥)) = 0 ))
6863, 65, 673anbi123d 1433 . . . . 5 (𝑛 = → ((((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 ) ↔ ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 )))
69682ralbidv 3128 . . . 4 (𝑛 = → (∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 ) ↔ ∀𝑥𝐵𝑦𝐵 ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 )))
7054, 69ceqsexv 3458 . . 3 (∃𝑛(𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 )) ↔ ∀𝑥𝐵𝑦𝐵 ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 ))
7153, 70anbi12i 629 . 2 (((𝐾 ∈ Poset ∧ (𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺)) ∧ ∃𝑛(𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 ))) ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ∧ ∀𝑥𝐵𝑦𝐵 ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 )))
7250, 51, 713bitr2i 302 1 (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ∧ ∀𝑥𝐵𝑦𝐵 ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 )))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∀wral 3070   class class class wbr 5032  dom cdm 5524  ‘cfv 6335  (class class class)co 7150  Basecbs 16541  lecple 16630  occoc 16631  Posetcpo 17616  lubclub 17618  glbcglb 17619  joincjn 17620  meetcmee 17621  0.cp0 17713  1.cp1 17714  OPcops 36748 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-nul 5176 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-dm 5534  df-iota 6294  df-fv 6343  df-ov 7153  df-oposet 36752 This theorem is referenced by:  opposet  36757  oposlem  36758  op01dm  36759
 Copyright terms: Public domain W3C validator