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

Theorem isopos 35201
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 6411 . . . . . . 7 (𝑝 = 𝐾 → (Base‘𝑝) = (Base‘𝐾))
2 isopos.b . . . . . . 7 𝐵 = (Base‘𝐾)
31, 2syl6eqr 2851 . . . . . 6 (𝑝 = 𝐾 → (Base‘𝑝) = 𝐵)
4 fveq2 6411 . . . . . . . 8 (𝑝 = 𝐾 → (lub‘𝑝) = (lub‘𝐾))
5 isopos.e . . . . . . . 8 𝑈 = (lub‘𝐾)
64, 5syl6eqr 2851 . . . . . . 7 (𝑝 = 𝐾 → (lub‘𝑝) = 𝑈)
76dmeqd 5529 . . . . . 6 (𝑝 = 𝐾 → dom (lub‘𝑝) = dom 𝑈)
83, 7eleq12d 2872 . . . . 5 (𝑝 = 𝐾 → ((Base‘𝑝) ∈ dom (lub‘𝑝) ↔ 𝐵 ∈ dom 𝑈))
9 fveq2 6411 . . . . . . . 8 (𝑝 = 𝐾 → (glb‘𝑝) = (glb‘𝐾))
10 isopos.g . . . . . . . 8 𝐺 = (glb‘𝐾)
119, 10syl6eqr 2851 . . . . . . 7 (𝑝 = 𝐾 → (glb‘𝑝) = 𝐺)
1211dmeqd 5529 . . . . . 6 (𝑝 = 𝐾 → dom (glb‘𝑝) = dom 𝐺)
133, 12eleq12d 2872 . . . . 5 (𝑝 = 𝐾 → ((Base‘𝑝) ∈ dom (glb‘𝑝) ↔ 𝐵 ∈ dom 𝐺))
148, 13anbi12d 625 . . . 4 (𝑝 = 𝐾 → (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ↔ (𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺)))
15 fveq2 6411 . . . . . . . 8 (𝑝 = 𝐾 → (oc‘𝑝) = (oc‘𝐾))
16 isopos.o . . . . . . . 8 = (oc‘𝐾)
1715, 16syl6eqr 2851 . . . . . . 7 (𝑝 = 𝐾 → (oc‘𝑝) = )
1817eqeq2d 2809 . . . . . 6 (𝑝 = 𝐾 → (𝑛 = (oc‘𝑝) ↔ 𝑛 = ))
193eleq2d 2864 . . . . . . . . . 10 (𝑝 = 𝐾 → ((𝑛𝑥) ∈ (Base‘𝑝) ↔ (𝑛𝑥) ∈ 𝐵))
20 fveq2 6411 . . . . . . . . . . . . 13 (𝑝 = 𝐾 → (le‘𝑝) = (le‘𝐾))
21 isopos.l . . . . . . . . . . . . 13 = (le‘𝐾)
2220, 21syl6eqr 2851 . . . . . . . . . . . 12 (𝑝 = 𝐾 → (le‘𝑝) = )
2322breqd 4854 . . . . . . . . . . 11 (𝑝 = 𝐾 → (𝑥(le‘𝑝)𝑦𝑥 𝑦))
2422breqd 4854 . . . . . . . . . . 11 (𝑝 = 𝐾 → ((𝑛𝑦)(le‘𝑝)(𝑛𝑥) ↔ (𝑛𝑦) (𝑛𝑥)))
2523, 24imbi12d 336 . . . . . . . . . 10 (𝑝 = 𝐾 → ((𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥)) ↔ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))))
2619, 253anbi13d 1563 . . . . . . . . 9 (𝑝 = 𝐾 → (((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ↔ ((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥)))))
27 fveq2 6411 . . . . . . . . . . . 12 (𝑝 = 𝐾 → (join‘𝑝) = (join‘𝐾))
28 isopos.j . . . . . . . . . . . 12 = (join‘𝐾)
2927, 28syl6eqr 2851 . . . . . . . . . . 11 (𝑝 = 𝐾 → (join‘𝑝) = )
3029oveqd 6895 . . . . . . . . . 10 (𝑝 = 𝐾 → (𝑥(join‘𝑝)(𝑛𝑥)) = (𝑥 (𝑛𝑥)))
31 fveq2 6411 . . . . . . . . . . 11 (𝑝 = 𝐾 → (1.‘𝑝) = (1.‘𝐾))
32 isopos.u . . . . . . . . . . 11 1 = (1.‘𝐾)
3331, 32syl6eqr 2851 . . . . . . . . . 10 (𝑝 = 𝐾 → (1.‘𝑝) = 1 )
3430, 33eqeq12d 2814 . . . . . . . . 9 (𝑝 = 𝐾 → ((𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ↔ (𝑥 (𝑛𝑥)) = 1 ))
35 fveq2 6411 . . . . . . . . . . . 12 (𝑝 = 𝐾 → (meet‘𝑝) = (meet‘𝐾))
36 isopos.m . . . . . . . . . . . 12 = (meet‘𝐾)
3735, 36syl6eqr 2851 . . . . . . . . . . 11 (𝑝 = 𝐾 → (meet‘𝑝) = )
3837oveqd 6895 . . . . . . . . . 10 (𝑝 = 𝐾 → (𝑥(meet‘𝑝)(𝑛𝑥)) = (𝑥 (𝑛𝑥)))
39 fveq2 6411 . . . . . . . . . . 11 (𝑝 = 𝐾 → (0.‘𝑝) = (0.‘𝐾))
40 isopos.f . . . . . . . . . . 11 0 = (0.‘𝐾)
4139, 40syl6eqr 2851 . . . . . . . . . 10 (𝑝 = 𝐾 → (0.‘𝑝) = 0 )
4238, 41eqeq12d 2814 . . . . . . . . 9 (𝑝 = 𝐾 → ((𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝) ↔ (𝑥 (𝑛𝑥)) = 0 ))
4326, 34, 423anbi123d 1561 . . . . . . . 8 (𝑝 = 𝐾 → ((((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ∧ (𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝)) ↔ (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 )))
443, 43raleqbidv 3335 . . . . . . 7 (𝑝 = 𝐾 → (∀𝑦 ∈ (Base‘𝑝)(((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ∧ (𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝)) ↔ ∀𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 )))
453, 44raleqbidv 3335 . . . . . 6 (𝑝 = 𝐾 → (∀𝑥 ∈ (Base‘𝑝)∀𝑦 ∈ (Base‘𝑝)(((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ∧ (𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝)) ↔ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 )))
4618, 45anbi12d 625 . . . . 5 (𝑝 = 𝐾 → ((𝑛 = (oc‘𝑝) ∧ ∀𝑥 ∈ (Base‘𝑝)∀𝑦 ∈ (Base‘𝑝)(((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ∧ (𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝))) ↔ (𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 ))))
4746exbidv 2017 . . . 4 (𝑝 = 𝐾 → (∃𝑛(𝑛 = (oc‘𝑝) ∧ ∀𝑥 ∈ (Base‘𝑝)∀𝑦 ∈ (Base‘𝑝)(((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ∧ (𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝))) ↔ ∃𝑛(𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 ))))
4814, 47anbi12d 625 . . 3 (𝑝 = 𝐾 → ((((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑛(𝑛 = (oc‘𝑝) ∧ ∀𝑥 ∈ (Base‘𝑝)∀𝑦 ∈ (Base‘𝑝)(((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ∧ (𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝)))) ↔ ((𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ∧ ∃𝑛(𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 )))))
49 df-oposet 35197 . . 3 OP = {𝑝 ∈ Poset ∣ (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑛(𝑛 = (oc‘𝑝) ∧ ∀𝑥 ∈ (Base‘𝑝)∀𝑦 ∈ (Base‘𝑝)(((𝑛𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛𝑦)(le‘𝑝)(𝑛𝑥))) ∧ (𝑥(join‘𝑝)(𝑛𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛𝑥)) = (0.‘𝑝))))}
5048, 49elrab2 3560 . 2 (𝐾 ∈ OP ↔ (𝐾 ∈ Poset ∧ ((𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ∧ ∃𝑛(𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 )))))
51 anass 461 . 2 (((𝐾 ∈ Poset ∧ (𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺)) ∧ ∃𝑛(𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 ))) ↔ (𝐾 ∈ Poset ∧ ((𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ∧ ∃𝑛(𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 )))))
52 3anass 1117 . . . 4 ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ↔ (𝐾 ∈ Poset ∧ (𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺)))
5352bicomi 216 . . 3 ((𝐾 ∈ Poset ∧ (𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺)) ↔ (𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺))
5416fvexi 6425 . . . 4 ∈ V
55 fveq1 6410 . . . . . . . 8 (𝑛 = → (𝑛𝑥) = ( 𝑥))
5655eleq1d 2863 . . . . . . 7 (𝑛 = → ((𝑛𝑥) ∈ 𝐵 ↔ ( 𝑥) ∈ 𝐵))
57 id 22 . . . . . . . . 9 (𝑛 = 𝑛 = )
5857, 55fveq12d 6418 . . . . . . . 8 (𝑛 = → (𝑛‘(𝑛𝑥)) = ( ‘( 𝑥)))
5958eqeq1d 2801 . . . . . . 7 (𝑛 = → ((𝑛‘(𝑛𝑥)) = 𝑥 ↔ ( ‘( 𝑥)) = 𝑥))
60 fveq1 6410 . . . . . . . . 9 (𝑛 = → (𝑛𝑦) = ( 𝑦))
6160, 55breq12d 4856 . . . . . . . 8 (𝑛 = → ((𝑛𝑦) (𝑛𝑥) ↔ ( 𝑦) ( 𝑥)))
6261imbi2d 332 . . . . . . 7 (𝑛 = → ((𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥)) ↔ (𝑥 𝑦 → ( 𝑦) ( 𝑥))))
6356, 59, 623anbi123d 1561 . . . . . 6 (𝑛 = → (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ↔ (( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥)))))
6455oveq2d 6894 . . . . . . 7 (𝑛 = → (𝑥 (𝑛𝑥)) = (𝑥 ( 𝑥)))
6564eqeq1d 2801 . . . . . 6 (𝑛 = → ((𝑥 (𝑛𝑥)) = 1 ↔ (𝑥 ( 𝑥)) = 1 ))
6655oveq2d 6894 . . . . . . 7 (𝑛 = → (𝑥 (𝑛𝑥)) = (𝑥 ( 𝑥)))
6766eqeq1d 2801 . . . . . 6 (𝑛 = → ((𝑥 (𝑛𝑥)) = 0 ↔ (𝑥 ( 𝑥)) = 0 ))
6863, 65, 673anbi123d 1561 . . . . 5 (𝑛 = → ((((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 ) ↔ ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 )))
69682ralbidv 3170 . . . 4 (𝑛 = → (∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 ) ↔ ∀𝑥𝐵𝑦𝐵 ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 )))
7054, 69ceqsexv 3430 . . 3 (∃𝑛(𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 )) ↔ ∀𝑥𝐵𝑦𝐵 ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 ))
7153, 70anbi12i 621 . 2 (((𝐾 ∈ Poset ∧ (𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺)) ∧ ∃𝑛(𝑛 = ∧ ∀𝑥𝐵𝑦𝐵 (((𝑛𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛𝑥)) = 𝑥 ∧ (𝑥 𝑦 → (𝑛𝑦) (𝑛𝑥))) ∧ (𝑥 (𝑛𝑥)) = 1 ∧ (𝑥 (𝑛𝑥)) = 0 ))) ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ∧ ∀𝑥𝐵𝑦𝐵 ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 )))
7250, 51, 713bitr2i 291 1 (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ∧ ∀𝑥𝐵𝑦𝐵 ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385  w3a 1108   = wceq 1653  wex 1875  wcel 2157  wral 3089   class class class wbr 4843  dom cdm 5312  cfv 6101  (class class class)co 6878  Basecbs 16184  lecple 16274  occoc 16275  Posetcpo 17255  lubclub 17257  glbcglb 17258  joincjn 17259  meetcmee 17260  0.cp0 17352  1.cp1 17353  OPcops 35193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-nul 4983
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-dm 5322  df-iota 6064  df-fv 6109  df-ov 6881  df-oposet 35197
This theorem is referenced by:  opposet  35202  oposlem  35203  op01dm  35204
  Copyright terms: Public domain W3C validator