Proof of Theorem ordtprsval
Step | Hyp | Ref
| Expression |
1 | | ordtNEW.l |
. . . 4
⊢ ≤ =
((le‘𝐾) ∩ (𝐵 × 𝐵)) |
2 | | fvex 6787 |
. . . . 5
⊢
(le‘𝐾) ∈
V |
3 | 2 | inex1 5241 |
. . . 4
⊢
((le‘𝐾) ∩
(𝐵 × 𝐵)) ∈ V |
4 | 1, 3 | eqeltri 2835 |
. . 3
⊢ ≤ ∈
V |
5 | | eqid 2738 |
. . . 4
⊢ dom ≤ = dom
≤ |
6 | | eqid 2738 |
. . . 4
⊢ ran
(𝑥 ∈ dom ≤ ↦
{𝑦 ∈ dom ≤ ∣
¬ 𝑦 ≤ 𝑥}) = ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) |
7 | | eqid 2738 |
. . . 4
⊢ ran
(𝑥 ∈ dom ≤ ↦
{𝑦 ∈ dom ≤ ∣
¬ 𝑥 ≤ 𝑦}) = ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}) |
8 | 5, 6, 7 | ordtval 22340 |
. . 3
⊢ ( ≤ ∈ V
→ (ordTop‘ ≤ ) =
(topGen‘(fi‘({dom ≤ } ∪ (ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦})))))) |
9 | 4, 8 | ax-mp 5 |
. 2
⊢
(ordTop‘ ≤ ) =
(topGen‘(fi‘({dom ≤ } ∪ (ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}))))) |
10 | | ordtNEW.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
11 | 10, 1 | prsdm 31864 |
. . . . . 6
⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵) |
12 | 11 | sneqd 4573 |
. . . . 5
⊢ (𝐾 ∈ Proset → {dom ≤ } = {𝐵}) |
13 | 11 | rabeqdv 3419 |
. . . . . . . . 9
⊢ (𝐾 ∈ Proset → {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) |
14 | 11, 13 | mpteq12dv 5165 |
. . . . . . . 8
⊢ (𝐾 ∈ Proset → (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})) |
15 | 14 | rneqd 5847 |
. . . . . . 7
⊢ (𝐾 ∈ Proset → ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})) |
16 | | ordtposval.e |
. . . . . . 7
⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) |
17 | 15, 16 | eqtr4di 2796 |
. . . . . 6
⊢ (𝐾 ∈ Proset → ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) = 𝐸) |
18 | 11 | rabeqdv 3419 |
. . . . . . . . 9
⊢ (𝐾 ∈ Proset → {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) |
19 | 11, 18 | mpteq12dv 5165 |
. . . . . . . 8
⊢ (𝐾 ∈ Proset → (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) |
20 | 19 | rneqd 5847 |
. . . . . . 7
⊢ (𝐾 ∈ Proset → ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) |
21 | | ordtposval.f |
. . . . . . 7
⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) |
22 | 20, 21 | eqtr4di 2796 |
. . . . . 6
⊢ (𝐾 ∈ Proset → ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}) = 𝐹) |
23 | 17, 22 | uneq12d 4098 |
. . . . 5
⊢ (𝐾 ∈ Proset → (ran
(𝑥 ∈ dom ≤ ↦
{𝑦 ∈ dom ≤ ∣
¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦})) = (𝐸 ∪ 𝐹)) |
24 | 12, 23 | uneq12d 4098 |
. . . 4
⊢ (𝐾 ∈ Proset → ({dom
≤ }
∪ (ran (𝑥 ∈ dom
≤
↦ {𝑦 ∈ dom ≤ ∣
¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}))) = ({𝐵} ∪ (𝐸 ∪ 𝐹))) |
25 | 24 | fveq2d 6778 |
. . 3
⊢ (𝐾 ∈ Proset →
(fi‘({dom ≤ } ∪ (ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦})))) = (fi‘({𝐵} ∪ (𝐸 ∪ 𝐹)))) |
26 | 25 | fveq2d 6778 |
. 2
⊢ (𝐾 ∈ Proset →
(topGen‘(fi‘({dom ≤ } ∪ (ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}))))) = (topGen‘(fi‘({𝐵} ∪ (𝐸 ∪ 𝐹))))) |
27 | 9, 26 | eqtrid 2790 |
1
⊢ (𝐾 ∈ Proset →
(ordTop‘ ≤ ) =
(topGen‘(fi‘({𝐵} ∪ (𝐸 ∪ 𝐹))))) |