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 37645
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 6843 . . . . . . 7 (𝑝 = 𝐾 β†’ (Baseβ€˜π‘) = (Baseβ€˜πΎ))
2 isopos.b . . . . . . 7 𝐡 = (Baseβ€˜πΎ)
31, 2eqtr4di 2795 . . . . . 6 (𝑝 = 𝐾 β†’ (Baseβ€˜π‘) = 𝐡)
4 fveq2 6843 . . . . . . . 8 (𝑝 = 𝐾 β†’ (lubβ€˜π‘) = (lubβ€˜πΎ))
5 isopos.e . . . . . . . 8 π‘ˆ = (lubβ€˜πΎ)
64, 5eqtr4di 2795 . . . . . . 7 (𝑝 = 𝐾 β†’ (lubβ€˜π‘) = π‘ˆ)
76dmeqd 5862 . . . . . 6 (𝑝 = 𝐾 β†’ dom (lubβ€˜π‘) = dom π‘ˆ)
83, 7eleq12d 2832 . . . . 5 (𝑝 = 𝐾 β†’ ((Baseβ€˜π‘) ∈ dom (lubβ€˜π‘) ↔ 𝐡 ∈ dom π‘ˆ))
9 fveq2 6843 . . . . . . . 8 (𝑝 = 𝐾 β†’ (glbβ€˜π‘) = (glbβ€˜πΎ))
10 isopos.g . . . . . . . 8 𝐺 = (glbβ€˜πΎ)
119, 10eqtr4di 2795 . . . . . . 7 (𝑝 = 𝐾 β†’ (glbβ€˜π‘) = 𝐺)
1211dmeqd 5862 . . . . . 6 (𝑝 = 𝐾 β†’ dom (glbβ€˜π‘) = dom 𝐺)
133, 12eleq12d 2832 . . . . 5 (𝑝 = 𝐾 β†’ ((Baseβ€˜π‘) ∈ dom (glbβ€˜π‘) ↔ 𝐡 ∈ dom 𝐺))
148, 13anbi12d 632 . . . 4 (𝑝 = 𝐾 β†’ (((Baseβ€˜π‘) ∈ dom (lubβ€˜π‘) ∧ (Baseβ€˜π‘) ∈ dom (glbβ€˜π‘)) ↔ (𝐡 ∈ dom π‘ˆ ∧ 𝐡 ∈ dom 𝐺)))
15 fveq2 6843 . . . . . . . 8 (𝑝 = 𝐾 β†’ (ocβ€˜π‘) = (ocβ€˜πΎ))
16 isopos.o . . . . . . . 8 βŠ₯ = (ocβ€˜πΎ)
1715, 16eqtr4di 2795 . . . . . . 7 (𝑝 = 𝐾 β†’ (ocβ€˜π‘) = βŠ₯ )
1817eqeq2d 2748 . . . . . 6 (𝑝 = 𝐾 β†’ (𝑛 = (ocβ€˜π‘) ↔ 𝑛 = βŠ₯ ))
193eleq2d 2824 . . . . . . . . . 10 (𝑝 = 𝐾 β†’ ((π‘›β€˜π‘₯) ∈ (Baseβ€˜π‘) ↔ (π‘›β€˜π‘₯) ∈ 𝐡))
20 fveq2 6843 . . . . . . . . . . . . 13 (𝑝 = 𝐾 β†’ (leβ€˜π‘) = (leβ€˜πΎ))
21 isopos.l . . . . . . . . . . . . 13 ≀ = (leβ€˜πΎ)
2220, 21eqtr4di 2795 . . . . . . . . . . . 12 (𝑝 = 𝐾 β†’ (leβ€˜π‘) = ≀ )
2322breqd 5117 . . . . . . . . . . 11 (𝑝 = 𝐾 β†’ (π‘₯(leβ€˜π‘)𝑦 ↔ π‘₯ ≀ 𝑦))
2422breqd 5117 . . . . . . . . . . 11 (𝑝 = 𝐾 β†’ ((π‘›β€˜π‘¦)(leβ€˜π‘)(π‘›β€˜π‘₯) ↔ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯)))
2523, 24imbi12d 345 . . . . . . . . . 10 (𝑝 = 𝐾 β†’ ((π‘₯(leβ€˜π‘)𝑦 β†’ (π‘›β€˜π‘¦)(leβ€˜π‘)(π‘›β€˜π‘₯)) ↔ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯))))
2619, 253anbi13d 1439 . . . . . . . . 9 (𝑝 = 𝐾 β†’ (((π‘›β€˜π‘₯) ∈ (Baseβ€˜π‘) ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯(leβ€˜π‘)𝑦 β†’ (π‘›β€˜π‘¦)(leβ€˜π‘)(π‘›β€˜π‘₯))) ↔ ((π‘›β€˜π‘₯) ∈ 𝐡 ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯)))))
27 fveq2 6843 . . . . . . . . . . . 12 (𝑝 = 𝐾 β†’ (joinβ€˜π‘) = (joinβ€˜πΎ))
28 isopos.j . . . . . . . . . . . 12 ∨ = (joinβ€˜πΎ)
2927, 28eqtr4di 2795 . . . . . . . . . . 11 (𝑝 = 𝐾 β†’ (joinβ€˜π‘) = ∨ )
3029oveqd 7375 . . . . . . . . . 10 (𝑝 = 𝐾 β†’ (π‘₯(joinβ€˜π‘)(π‘›β€˜π‘₯)) = (π‘₯ ∨ (π‘›β€˜π‘₯)))
31 fveq2 6843 . . . . . . . . . . 11 (𝑝 = 𝐾 β†’ (1.β€˜π‘) = (1.β€˜πΎ))
32 isopos.u . . . . . . . . . . 11 1 = (1.β€˜πΎ)
3331, 32eqtr4di 2795 . . . . . . . . . 10 (𝑝 = 𝐾 β†’ (1.β€˜π‘) = 1 )
3430, 33eqeq12d 2753 . . . . . . . . 9 (𝑝 = 𝐾 β†’ ((π‘₯(joinβ€˜π‘)(π‘›β€˜π‘₯)) = (1.β€˜π‘) ↔ (π‘₯ ∨ (π‘›β€˜π‘₯)) = 1 ))
35 fveq2 6843 . . . . . . . . . . . 12 (𝑝 = 𝐾 β†’ (meetβ€˜π‘) = (meetβ€˜πΎ))
36 isopos.m . . . . . . . . . . . 12 ∧ = (meetβ€˜πΎ)
3735, 36eqtr4di 2795 . . . . . . . . . . 11 (𝑝 = 𝐾 β†’ (meetβ€˜π‘) = ∧ )
3837oveqd 7375 . . . . . . . . . 10 (𝑝 = 𝐾 β†’ (π‘₯(meetβ€˜π‘)(π‘›β€˜π‘₯)) = (π‘₯ ∧ (π‘›β€˜π‘₯)))
39 fveq2 6843 . . . . . . . . . . 11 (𝑝 = 𝐾 β†’ (0.β€˜π‘) = (0.β€˜πΎ))
40 isopos.f . . . . . . . . . . 11 0 = (0.β€˜πΎ)
4139, 40eqtr4di 2795 . . . . . . . . . 10 (𝑝 = 𝐾 β†’ (0.β€˜π‘) = 0 )
4238, 41eqeq12d 2753 . . . . . . . . 9 (𝑝 = 𝐾 β†’ ((π‘₯(meetβ€˜π‘)(π‘›β€˜π‘₯)) = (0.β€˜π‘) ↔ (π‘₯ ∧ (π‘›β€˜π‘₯)) = 0 ))
4326, 34, 423anbi123d 1437 . . . . . . . 8 (𝑝 = 𝐾 β†’ ((((π‘›β€˜π‘₯) ∈ (Baseβ€˜π‘) ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯(leβ€˜π‘)𝑦 β†’ (π‘›β€˜π‘¦)(leβ€˜π‘)(π‘›β€˜π‘₯))) ∧ (π‘₯(joinβ€˜π‘)(π‘›β€˜π‘₯)) = (1.β€˜π‘) ∧ (π‘₯(meetβ€˜π‘)(π‘›β€˜π‘₯)) = (0.β€˜π‘)) ↔ (((π‘›β€˜π‘₯) ∈ 𝐡 ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯))) ∧ (π‘₯ ∨ (π‘›β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ (π‘›β€˜π‘₯)) = 0 )))
443, 43raleqbidv 3320 . . . . . . 7 (𝑝 = 𝐾 β†’ (βˆ€π‘¦ ∈ (Baseβ€˜π‘)(((π‘›β€˜π‘₯) ∈ (Baseβ€˜π‘) ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯(leβ€˜π‘)𝑦 β†’ (π‘›β€˜π‘¦)(leβ€˜π‘)(π‘›β€˜π‘₯))) ∧ (π‘₯(joinβ€˜π‘)(π‘›β€˜π‘₯)) = (1.β€˜π‘) ∧ (π‘₯(meetβ€˜π‘)(π‘›β€˜π‘₯)) = (0.β€˜π‘)) ↔ βˆ€π‘¦ ∈ 𝐡 (((π‘›β€˜π‘₯) ∈ 𝐡 ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯))) ∧ (π‘₯ ∨ (π‘›β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ (π‘›β€˜π‘₯)) = 0 )))
453, 44raleqbidv 3320 . . . . . 6 (𝑝 = 𝐾 β†’ (βˆ€π‘₯ ∈ (Baseβ€˜π‘)βˆ€π‘¦ ∈ (Baseβ€˜π‘)(((π‘›β€˜π‘₯) ∈ (Baseβ€˜π‘) ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯(leβ€˜π‘)𝑦 β†’ (π‘›β€˜π‘¦)(leβ€˜π‘)(π‘›β€˜π‘₯))) ∧ (π‘₯(joinβ€˜π‘)(π‘›β€˜π‘₯)) = (1.β€˜π‘) ∧ (π‘₯(meetβ€˜π‘)(π‘›β€˜π‘₯)) = (0.β€˜π‘)) ↔ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (((π‘›β€˜π‘₯) ∈ 𝐡 ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯))) ∧ (π‘₯ ∨ (π‘›β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ (π‘›β€˜π‘₯)) = 0 )))
4618, 45anbi12d 632 . . . . 5 (𝑝 = 𝐾 β†’ ((𝑛 = (ocβ€˜π‘) ∧ βˆ€π‘₯ ∈ (Baseβ€˜π‘)βˆ€π‘¦ ∈ (Baseβ€˜π‘)(((π‘›β€˜π‘₯) ∈ (Baseβ€˜π‘) ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯(leβ€˜π‘)𝑦 β†’ (π‘›β€˜π‘¦)(leβ€˜π‘)(π‘›β€˜π‘₯))) ∧ (π‘₯(joinβ€˜π‘)(π‘›β€˜π‘₯)) = (1.β€˜π‘) ∧ (π‘₯(meetβ€˜π‘)(π‘›β€˜π‘₯)) = (0.β€˜π‘))) ↔ (𝑛 = βŠ₯ ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (((π‘›β€˜π‘₯) ∈ 𝐡 ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯))) ∧ (π‘₯ ∨ (π‘›β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ (π‘›β€˜π‘₯)) = 0 ))))
4746exbidv 1925 . . . 4 (𝑝 = 𝐾 β†’ (βˆƒπ‘›(𝑛 = (ocβ€˜π‘) ∧ βˆ€π‘₯ ∈ (Baseβ€˜π‘)βˆ€π‘¦ ∈ (Baseβ€˜π‘)(((π‘›β€˜π‘₯) ∈ (Baseβ€˜π‘) ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯(leβ€˜π‘)𝑦 β†’ (π‘›β€˜π‘¦)(leβ€˜π‘)(π‘›β€˜π‘₯))) ∧ (π‘₯(joinβ€˜π‘)(π‘›β€˜π‘₯)) = (1.β€˜π‘) ∧ (π‘₯(meetβ€˜π‘)(π‘›β€˜π‘₯)) = (0.β€˜π‘))) ↔ βˆƒπ‘›(𝑛 = βŠ₯ ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (((π‘›β€˜π‘₯) ∈ 𝐡 ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯))) ∧ (π‘₯ ∨ (π‘›β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ (π‘›β€˜π‘₯)) = 0 ))))
4814, 47anbi12d 632 . . 3 (𝑝 = 𝐾 β†’ ((((Baseβ€˜π‘) ∈ dom (lubβ€˜π‘) ∧ (Baseβ€˜π‘) ∈ dom (glbβ€˜π‘)) ∧ βˆƒπ‘›(𝑛 = (ocβ€˜π‘) ∧ βˆ€π‘₯ ∈ (Baseβ€˜π‘)βˆ€π‘¦ ∈ (Baseβ€˜π‘)(((π‘›β€˜π‘₯) ∈ (Baseβ€˜π‘) ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯(leβ€˜π‘)𝑦 β†’ (π‘›β€˜π‘¦)(leβ€˜π‘)(π‘›β€˜π‘₯))) ∧ (π‘₯(joinβ€˜π‘)(π‘›β€˜π‘₯)) = (1.β€˜π‘) ∧ (π‘₯(meetβ€˜π‘)(π‘›β€˜π‘₯)) = (0.β€˜π‘)))) ↔ ((𝐡 ∈ dom π‘ˆ ∧ 𝐡 ∈ dom 𝐺) ∧ βˆƒπ‘›(𝑛 = βŠ₯ ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (((π‘›β€˜π‘₯) ∈ 𝐡 ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯))) ∧ (π‘₯ ∨ (π‘›β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ (π‘›β€˜π‘₯)) = 0 )))))
49 df-oposet 37641 . . 3 OP = {𝑝 ∈ Poset ∣ (((Baseβ€˜π‘) ∈ dom (lubβ€˜π‘) ∧ (Baseβ€˜π‘) ∈ dom (glbβ€˜π‘)) ∧ βˆƒπ‘›(𝑛 = (ocβ€˜π‘) ∧ βˆ€π‘₯ ∈ (Baseβ€˜π‘)βˆ€π‘¦ ∈ (Baseβ€˜π‘)(((π‘›β€˜π‘₯) ∈ (Baseβ€˜π‘) ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯(leβ€˜π‘)𝑦 β†’ (π‘›β€˜π‘¦)(leβ€˜π‘)(π‘›β€˜π‘₯))) ∧ (π‘₯(joinβ€˜π‘)(π‘›β€˜π‘₯)) = (1.β€˜π‘) ∧ (π‘₯(meetβ€˜π‘)(π‘›β€˜π‘₯)) = (0.β€˜π‘))))}
5048, 49elrab2 3649 . 2 (𝐾 ∈ OP ↔ (𝐾 ∈ Poset ∧ ((𝐡 ∈ dom π‘ˆ ∧ 𝐡 ∈ dom 𝐺) ∧ βˆƒπ‘›(𝑛 = βŠ₯ ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (((π‘›β€˜π‘₯) ∈ 𝐡 ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯))) ∧ (π‘₯ ∨ (π‘›β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ (π‘›β€˜π‘₯)) = 0 )))))
51 anass 470 . 2 (((𝐾 ∈ Poset ∧ (𝐡 ∈ dom π‘ˆ ∧ 𝐡 ∈ dom 𝐺)) ∧ βˆƒπ‘›(𝑛 = βŠ₯ ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (((π‘›β€˜π‘₯) ∈ 𝐡 ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯))) ∧ (π‘₯ ∨ (π‘›β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ (π‘›β€˜π‘₯)) = 0 ))) ↔ (𝐾 ∈ Poset ∧ ((𝐡 ∈ dom π‘ˆ ∧ 𝐡 ∈ dom 𝐺) ∧ βˆƒπ‘›(𝑛 = βŠ₯ ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (((π‘›β€˜π‘₯) ∈ 𝐡 ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯))) ∧ (π‘₯ ∨ (π‘›β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ (π‘›β€˜π‘₯)) = 0 )))))
52 3anass 1096 . . . 4 ((𝐾 ∈ Poset ∧ 𝐡 ∈ dom π‘ˆ ∧ 𝐡 ∈ dom 𝐺) ↔ (𝐾 ∈ Poset ∧ (𝐡 ∈ dom π‘ˆ ∧ 𝐡 ∈ dom 𝐺)))
5352bicomi 223 . . 3 ((𝐾 ∈ Poset ∧ (𝐡 ∈ dom π‘ˆ ∧ 𝐡 ∈ dom 𝐺)) ↔ (𝐾 ∈ Poset ∧ 𝐡 ∈ dom π‘ˆ ∧ 𝐡 ∈ dom 𝐺))
5416fvexi 6857 . . . 4 βŠ₯ ∈ V
55 fveq1 6842 . . . . . . . 8 (𝑛 = βŠ₯ β†’ (π‘›β€˜π‘₯) = ( βŠ₯ β€˜π‘₯))
5655eleq1d 2823 . . . . . . 7 (𝑛 = βŠ₯ β†’ ((π‘›β€˜π‘₯) ∈ 𝐡 ↔ ( βŠ₯ β€˜π‘₯) ∈ 𝐡))
57 id 22 . . . . . . . . 9 (𝑛 = βŠ₯ β†’ 𝑛 = βŠ₯ )
5857, 55fveq12d 6850 . . . . . . . 8 (𝑛 = βŠ₯ β†’ (π‘›β€˜(π‘›β€˜π‘₯)) = ( βŠ₯ β€˜( βŠ₯ β€˜π‘₯)))
5958eqeq1d 2739 . . . . . . 7 (𝑛 = βŠ₯ β†’ ((π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ↔ ( βŠ₯ β€˜( βŠ₯ β€˜π‘₯)) = π‘₯))
60 fveq1 6842 . . . . . . . . 9 (𝑛 = βŠ₯ β†’ (π‘›β€˜π‘¦) = ( βŠ₯ β€˜π‘¦))
6160, 55breq12d 5119 . . . . . . . 8 (𝑛 = βŠ₯ β†’ ((π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯) ↔ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘₯)))
6261imbi2d 341 . . . . . . 7 (𝑛 = βŠ₯ β†’ ((π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯)) ↔ (π‘₯ ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘₯))))
6356, 59, 623anbi123d 1437 . . . . . 6 (𝑛 = βŠ₯ β†’ (((π‘›β€˜π‘₯) ∈ 𝐡 ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯))) ↔ (( βŠ₯ β€˜π‘₯) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘₯)))))
6455oveq2d 7374 . . . . . . 7 (𝑛 = βŠ₯ β†’ (π‘₯ ∨ (π‘›β€˜π‘₯)) = (π‘₯ ∨ ( βŠ₯ β€˜π‘₯)))
6564eqeq1d 2739 . . . . . 6 (𝑛 = βŠ₯ β†’ ((π‘₯ ∨ (π‘›β€˜π‘₯)) = 1 ↔ (π‘₯ ∨ ( βŠ₯ β€˜π‘₯)) = 1 ))
6655oveq2d 7374 . . . . . . 7 (𝑛 = βŠ₯ β†’ (π‘₯ ∧ (π‘›β€˜π‘₯)) = (π‘₯ ∧ ( βŠ₯ β€˜π‘₯)))
6766eqeq1d 2739 . . . . . 6 (𝑛 = βŠ₯ β†’ ((π‘₯ ∧ (π‘›β€˜π‘₯)) = 0 ↔ (π‘₯ ∧ ( βŠ₯ β€˜π‘₯)) = 0 ))
6863, 65, 673anbi123d 1437 . . . . 5 (𝑛 = βŠ₯ β†’ ((((π‘›β€˜π‘₯) ∈ 𝐡 ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯))) ∧ (π‘₯ ∨ (π‘›β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ (π‘›β€˜π‘₯)) = 0 ) ↔ ((( βŠ₯ β€˜π‘₯) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘₯))) ∧ (π‘₯ ∨ ( βŠ₯ β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ ( βŠ₯ β€˜π‘₯)) = 0 )))
69682ralbidv 3213 . . . 4 (𝑛 = βŠ₯ β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (((π‘›β€˜π‘₯) ∈ 𝐡 ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯))) ∧ (π‘₯ ∨ (π‘›β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ (π‘›β€˜π‘₯)) = 0 ) ↔ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((( βŠ₯ β€˜π‘₯) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘₯))) ∧ (π‘₯ ∨ ( βŠ₯ β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ ( βŠ₯ β€˜π‘₯)) = 0 )))
7054, 69ceqsexv 3495 . . 3 (βˆƒπ‘›(𝑛 = βŠ₯ ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (((π‘›β€˜π‘₯) ∈ 𝐡 ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯))) ∧ (π‘₯ ∨ (π‘›β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ (π‘›β€˜π‘₯)) = 0 )) ↔ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((( βŠ₯ β€˜π‘₯) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘₯))) ∧ (π‘₯ ∨ ( βŠ₯ β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ ( βŠ₯ β€˜π‘₯)) = 0 ))
7153, 70anbi12i 628 . 2 (((𝐾 ∈ Poset ∧ (𝐡 ∈ dom π‘ˆ ∧ 𝐡 ∈ dom 𝐺)) ∧ βˆƒπ‘›(𝑛 = βŠ₯ ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (((π‘›β€˜π‘₯) ∈ 𝐡 ∧ (π‘›β€˜(π‘›β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ (π‘›β€˜π‘¦) ≀ (π‘›β€˜π‘₯))) ∧ (π‘₯ ∨ (π‘›β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ (π‘›β€˜π‘₯)) = 0 ))) ↔ ((𝐾 ∈ Poset ∧ 𝐡 ∈ dom π‘ˆ ∧ 𝐡 ∈ dom 𝐺) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((( βŠ₯ β€˜π‘₯) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘₯))) ∧ (π‘₯ ∨ ( βŠ₯ β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ ( βŠ₯ β€˜π‘₯)) = 0 )))
7250, 51, 713bitr2i 299 1 (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐡 ∈ dom π‘ˆ ∧ 𝐡 ∈ dom 𝐺) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((( βŠ₯ β€˜π‘₯) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘₯))) ∧ (π‘₯ ∨ ( βŠ₯ β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ ( βŠ₯ β€˜π‘₯)) = 0 )))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  βˆ€wral 3065   class class class wbr 5106  dom cdm 5634  β€˜cfv 6497  (class class class)co 7358  Basecbs 17084  lecple 17141  occoc 17142  Posetcpo 18197  lubclub 18199  glbcglb 18200  joincjn 18201  meetcmee 18202  0.cp0 18313  1.cp1 18314  OPcops 37637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-nul 5264
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-dm 5644  df-iota 6449  df-fv 6505  df-ov 7361  df-oposet 37641
This theorem is referenced by:  opposet  37646  oposlem  37647  op01dm  37648
  Copyright terms: Public domain W3C validator