| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑝 = 𝐾 → (Base‘𝑝) = (Base‘𝐾)) |
| 2 | | isopos.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
| 3 | 1, 2 | eqtr4di 2795 |
. . . . . 6
⊢ (𝑝 = 𝐾 → (Base‘𝑝) = 𝐵) |
| 4 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑝 = 𝐾 → (lub‘𝑝) = (lub‘𝐾)) |
| 5 | | isopos.e |
. . . . . . . 8
⊢ 𝑈 = (lub‘𝐾) |
| 6 | 4, 5 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑝 = 𝐾 → (lub‘𝑝) = 𝑈) |
| 7 | 6 | dmeqd 5916 |
. . . . . 6
⊢ (𝑝 = 𝐾 → dom (lub‘𝑝) = dom 𝑈) |
| 8 | 3, 7 | eleq12d 2835 |
. . . . 5
⊢ (𝑝 = 𝐾 → ((Base‘𝑝) ∈ dom (lub‘𝑝) ↔ 𝐵 ∈ dom 𝑈)) |
| 9 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑝 = 𝐾 → (glb‘𝑝) = (glb‘𝐾)) |
| 10 | | isopos.g |
. . . . . . . 8
⊢ 𝐺 = (glb‘𝐾) |
| 11 | 9, 10 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑝 = 𝐾 → (glb‘𝑝) = 𝐺) |
| 12 | 11 | dmeqd 5916 |
. . . . . 6
⊢ (𝑝 = 𝐾 → dom (glb‘𝑝) = dom 𝐺) |
| 13 | 3, 12 | eleq12d 2835 |
. . . . 5
⊢ (𝑝 = 𝐾 → ((Base‘𝑝) ∈ dom (glb‘𝑝) ↔ 𝐵 ∈ dom 𝐺)) |
| 14 | 8, 13 | anbi12d 632 |
. . . 4
⊢ (𝑝 = 𝐾 → (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ↔ (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺))) |
| 15 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑝 = 𝐾 → (oc‘𝑝) = (oc‘𝐾)) |
| 16 | | isopos.o |
. . . . . . . 8
⊢ ⊥ =
(oc‘𝐾) |
| 17 | 15, 16 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑝 = 𝐾 → (oc‘𝑝) = ⊥ ) |
| 18 | 17 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑝 = 𝐾 → (𝑛 = (oc‘𝑝) ↔ 𝑛 = ⊥ )) |
| 19 | 3 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑝 = 𝐾 → ((𝑛‘𝑥) ∈ (Base‘𝑝) ↔ (𝑛‘𝑥) ∈ 𝐵)) |
| 20 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝐾 → (le‘𝑝) = (le‘𝐾)) |
| 21 | | isopos.l |
. . . . . . . . . . . . 13
⊢ ≤ =
(le‘𝐾) |
| 22 | 20, 21 | eqtr4di 2795 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝐾 → (le‘𝑝) = ≤ ) |
| 23 | 22 | breqd 5154 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝐾 → (𝑥(le‘𝑝)𝑦 ↔ 𝑥 ≤ 𝑦)) |
| 24 | 22 | breqd 5154 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝐾 → ((𝑛‘𝑦)(le‘𝑝)(𝑛‘𝑥) ↔ (𝑛‘𝑦) ≤ (𝑛‘𝑥))) |
| 25 | 23, 24 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑝 = 𝐾 → ((𝑥(le‘𝑝)𝑦 → (𝑛‘𝑦)(le‘𝑝)(𝑛‘𝑥)) ↔ (𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥)))) |
| 26 | 19, 25 | 3anbi13d 1440 |
. . . . . . . . 9
⊢ (𝑝 = 𝐾 → (((𝑛‘𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛‘𝑦)(le‘𝑝)(𝑛‘𝑥))) ↔ ((𝑛‘𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥))))) |
| 27 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝐾 → (join‘𝑝) = (join‘𝐾)) |
| 28 | | isopos.j |
. . . . . . . . . . . 12
⊢ ∨ =
(join‘𝐾) |
| 29 | 27, 28 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝐾 → (join‘𝑝) = ∨ ) |
| 30 | 29 | oveqd 7448 |
. . . . . . . . . 10
⊢ (𝑝 = 𝐾 → (𝑥(join‘𝑝)(𝑛‘𝑥)) = (𝑥 ∨ (𝑛‘𝑥))) |
| 31 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝐾 → (1.‘𝑝) = (1.‘𝐾)) |
| 32 | | isopos.u |
. . . . . . . . . . 11
⊢ 1 =
(1.‘𝐾) |
| 33 | 31, 32 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝑝 = 𝐾 → (1.‘𝑝) = 1 ) |
| 34 | 30, 33 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (𝑝 = 𝐾 → ((𝑥(join‘𝑝)(𝑛‘𝑥)) = (1.‘𝑝) ↔ (𝑥 ∨ (𝑛‘𝑥)) = 1 )) |
| 35 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝐾 → (meet‘𝑝) = (meet‘𝐾)) |
| 36 | | isopos.m |
. . . . . . . . . . . 12
⊢ ∧ =
(meet‘𝐾) |
| 37 | 35, 36 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝐾 → (meet‘𝑝) = ∧ ) |
| 38 | 37 | oveqd 7448 |
. . . . . . . . . 10
⊢ (𝑝 = 𝐾 → (𝑥(meet‘𝑝)(𝑛‘𝑥)) = (𝑥 ∧ (𝑛‘𝑥))) |
| 39 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝐾 → (0.‘𝑝) = (0.‘𝐾)) |
| 40 | | isopos.f |
. . . . . . . . . . 11
⊢ 0 =
(0.‘𝐾) |
| 41 | 39, 40 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝑝 = 𝐾 → (0.‘𝑝) = 0 ) |
| 42 | 38, 41 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (𝑝 = 𝐾 → ((𝑥(meet‘𝑝)(𝑛‘𝑥)) = (0.‘𝑝) ↔ (𝑥 ∧ (𝑛‘𝑥)) = 0 )) |
| 43 | 26, 34, 42 | 3anbi123d 1438 |
. . . . . . . 8
⊢ (𝑝 = 𝐾 → ((((𝑛‘𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛‘𝑦)(le‘𝑝)(𝑛‘𝑥))) ∧ (𝑥(join‘𝑝)(𝑛‘𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛‘𝑥)) = (0.‘𝑝)) ↔ (((𝑛‘𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥))) ∧ (𝑥 ∨ (𝑛‘𝑥)) = 1 ∧ (𝑥 ∧ (𝑛‘𝑥)) = 0 ))) |
| 44 | 3, 43 | raleqbidv 3346 |
. . . . . . 7
⊢ (𝑝 = 𝐾 → (∀𝑦 ∈ (Base‘𝑝)(((𝑛‘𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛‘𝑦)(le‘𝑝)(𝑛‘𝑥))) ∧ (𝑥(join‘𝑝)(𝑛‘𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛‘𝑥)) = (0.‘𝑝)) ↔ ∀𝑦 ∈ 𝐵 (((𝑛‘𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥))) ∧ (𝑥 ∨ (𝑛‘𝑥)) = 1 ∧ (𝑥 ∧ (𝑛‘𝑥)) = 0 ))) |
| 45 | 3, 44 | raleqbidv 3346 |
. . . . . 6
⊢ (𝑝 = 𝐾 → (∀𝑥 ∈ (Base‘𝑝)∀𝑦 ∈ (Base‘𝑝)(((𝑛‘𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛‘𝑦)(le‘𝑝)(𝑛‘𝑥))) ∧ (𝑥(join‘𝑝)(𝑛‘𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛‘𝑥)) = (0.‘𝑝)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝑛‘𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥))) ∧ (𝑥 ∨ (𝑛‘𝑥)) = 1 ∧ (𝑥 ∧ (𝑛‘𝑥)) = 0 ))) |
| 46 | 18, 45 | anbi12d 632 |
. . . . 5
⊢ (𝑝 = 𝐾 → ((𝑛 = (oc‘𝑝) ∧ ∀𝑥 ∈ (Base‘𝑝)∀𝑦 ∈ (Base‘𝑝)(((𝑛‘𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛‘𝑦)(le‘𝑝)(𝑛‘𝑥))) ∧ (𝑥(join‘𝑝)(𝑛‘𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛‘𝑥)) = (0.‘𝑝))) ↔ (𝑛 = ⊥ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝑛‘𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥))) ∧ (𝑥 ∨ (𝑛‘𝑥)) = 1 ∧ (𝑥 ∧ (𝑛‘𝑥)) = 0 )))) |
| 47 | 46 | exbidv 1921 |
. . . 4
⊢ (𝑝 = 𝐾 → (∃𝑛(𝑛 = (oc‘𝑝) ∧ ∀𝑥 ∈ (Base‘𝑝)∀𝑦 ∈ (Base‘𝑝)(((𝑛‘𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛‘𝑦)(le‘𝑝)(𝑛‘𝑥))) ∧ (𝑥(join‘𝑝)(𝑛‘𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛‘𝑥)) = (0.‘𝑝))) ↔ ∃𝑛(𝑛 = ⊥ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝑛‘𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥))) ∧ (𝑥 ∨ (𝑛‘𝑥)) = 1 ∧ (𝑥 ∧ (𝑛‘𝑥)) = 0 )))) |
| 48 | 14, 47 | anbi12d 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 39177 |
. . 3
⊢ OP =
{𝑝 ∈ Poset ∣
(((Base‘𝑝) ∈ dom
(lub‘𝑝) ∧
(Base‘𝑝) ∈ dom
(glb‘𝑝)) ∧
∃𝑛(𝑛 = (oc‘𝑝) ∧ ∀𝑥 ∈ (Base‘𝑝)∀𝑦 ∈ (Base‘𝑝)(((𝑛‘𝑥) ∈ (Base‘𝑝) ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝑝)𝑦 → (𝑛‘𝑦)(le‘𝑝)(𝑛‘𝑥))) ∧ (𝑥(join‘𝑝)(𝑛‘𝑥)) = (1.‘𝑝) ∧ (𝑥(meet‘𝑝)(𝑛‘𝑥)) = (0.‘𝑝))))} |
| 50 | 48, 49 | elrab2 3695 |
. 2
⊢ (𝐾 ∈ OP ↔ (𝐾 ∈ Poset ∧ ((𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺) ∧ ∃𝑛(𝑛 = ⊥ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝑛‘𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥))) ∧ (𝑥 ∨ (𝑛‘𝑥)) = 1 ∧ (𝑥 ∧ (𝑛‘𝑥)) = 0 ))))) |
| 51 | | anass 468 |
. 2
⊢ (((𝐾 ∈ Poset ∧ (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺)) ∧ ∃𝑛(𝑛 = ⊥ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝑛‘𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥))) ∧ (𝑥 ∨ (𝑛‘𝑥)) = 1 ∧ (𝑥 ∧ (𝑛‘𝑥)) = 0 ))) ↔ (𝐾 ∈ Poset ∧ ((𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺) ∧ ∃𝑛(𝑛 = ⊥ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝑛‘𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥))) ∧ (𝑥 ∨ (𝑛‘𝑥)) = 1 ∧ (𝑥 ∧ (𝑛‘𝑥)) = 0 ))))) |
| 52 | | 3anass 1095 |
. . . 4
⊢ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺) ↔ (𝐾 ∈ Poset ∧ (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺))) |
| 53 | 52 | bicomi 224 |
. . 3
⊢ ((𝐾 ∈ Poset ∧ (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺)) ↔ (𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺)) |
| 54 | 16 | fvexi 6920 |
. . . 4
⊢ ⊥ ∈
V |
| 55 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑛 = ⊥ → (𝑛‘𝑥) = ( ⊥ ‘𝑥)) |
| 56 | 55 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑛 = ⊥ → ((𝑛‘𝑥) ∈ 𝐵 ↔ ( ⊥ ‘𝑥) ∈ 𝐵)) |
| 57 | | id 22 |
. . . . . . . . 9
⊢ (𝑛 = ⊥ → 𝑛 = ⊥ ) |
| 58 | 57, 55 | fveq12d 6913 |
. . . . . . . 8
⊢ (𝑛 = ⊥ → (𝑛‘(𝑛‘𝑥)) = ( ⊥ ‘( ⊥
‘𝑥))) |
| 59 | 58 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑛 = ⊥ → ((𝑛‘(𝑛‘𝑥)) = 𝑥 ↔ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)) |
| 60 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑛 = ⊥ → (𝑛‘𝑦) = ( ⊥ ‘𝑦)) |
| 61 | 60, 55 | breq12d 5156 |
. . . . . . . 8
⊢ (𝑛 = ⊥ → ((𝑛‘𝑦) ≤ (𝑛‘𝑥) ↔ ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) |
| 62 | 61 | imbi2d 340 |
. . . . . . 7
⊢ (𝑛 = ⊥ → ((𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥)) ↔ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥)))) |
| 63 | 56, 59, 62 | 3anbi123d 1438 |
. . . . . 6
⊢ (𝑛 = ⊥ → (((𝑛‘𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥))) ↔ (( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))))) |
| 64 | 55 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑛 = ⊥ → (𝑥 ∨ (𝑛‘𝑥)) = (𝑥 ∨ ( ⊥ ‘𝑥))) |
| 65 | 64 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑛 = ⊥ → ((𝑥 ∨ (𝑛‘𝑥)) = 1 ↔ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 )) |
| 66 | 55 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑛 = ⊥ → (𝑥 ∧ (𝑛‘𝑥)) = (𝑥 ∧ ( ⊥ ‘𝑥))) |
| 67 | 66 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑛 = ⊥ → ((𝑥 ∧ (𝑛‘𝑥)) = 0 ↔ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 )) |
| 68 | 63, 65, 67 | 3anbi123d 1438 |
. . . . 5
⊢ (𝑛 = ⊥ → ((((𝑛‘𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥))) ∧ (𝑥 ∨ (𝑛‘𝑥)) = 1 ∧ (𝑥 ∧ (𝑛‘𝑥)) = 0 ) ↔ ((( ⊥
‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 ))) |
| 69 | 68 | 2ralbidv 3221 |
. . . 4
⊢ (𝑛 = ⊥ →
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝑛‘𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥))) ∧ (𝑥 ∨ (𝑛‘𝑥)) = 1 ∧ (𝑥 ∧ (𝑛‘𝑥)) = 0 ) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 ))) |
| 70 | 54, 69 | ceqsexv 3532 |
. . 3
⊢
(∃𝑛(𝑛 = ⊥ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝑛‘𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥))) ∧ (𝑥 ∨ (𝑛‘𝑥)) = 1 ∧ (𝑥 ∧ (𝑛‘𝑥)) = 0 )) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 )) |
| 71 | 53, 70 | anbi12i 628 |
. 2
⊢ (((𝐾 ∈ Poset ∧ (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺)) ∧ ∃𝑛(𝑛 = ⊥ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝑛‘𝑥) ∈ 𝐵 ∧ (𝑛‘(𝑛‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → (𝑛‘𝑦) ≤ (𝑛‘𝑥))) ∧ (𝑥 ∨ (𝑛‘𝑥)) = 1 ∧ (𝑥 ∧ (𝑛‘𝑥)) = 0 ))) ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 ))) |
| 72 | 50, 51, 71 | 3bitr2i 299 |
1
⊢ (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 ))) |