Proof of Theorem ordtprsval
Step | Hyp | Ref
| Expression |
1 | | ordtNEW.l |
. . . 4
⊢ ≤ =
((le‘𝐾) ∩ (𝐵 × 𝐵)) |
2 | | fvex 6690 |
. . . . 5
⊢
(le‘𝐾) ∈
V |
3 | 2 | inex1 5186 |
. . . 4
⊢
((le‘𝐾) ∩
(𝐵 × 𝐵)) ∈ V |
4 | 1, 3 | eqeltri 2830 |
. . 3
⊢ ≤ ∈
V |
5 | | eqid 2739 |
. . . 4
⊢ dom ≤ = dom
≤ |
6 | | eqid 2739 |
. . . 4
⊢ ran
(𝑥 ∈ dom ≤ ↦
{𝑦 ∈ dom ≤ ∣
¬ 𝑦 ≤ 𝑥}) = ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) |
7 | | eqid 2739 |
. . . 4
⊢ ran
(𝑥 ∈ dom ≤ ↦
{𝑦 ∈ dom ≤ ∣
¬ 𝑥 ≤ 𝑦}) = ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}) |
8 | 5, 6, 7 | ordtval 21943 |
. . 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 31439 |
. . . . . 6
⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵) |
12 | 11 | sneqd 4529 |
. . . . 5
⊢ (𝐾 ∈ Proset → {dom ≤ } = {𝐵}) |
13 | 11 | rabeqdv 3387 |
. . . . . . . . 9
⊢ (𝐾 ∈ Proset → {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) |
14 | 11, 13 | mpteq12dv 5116 |
. . . . . . . 8
⊢ (𝐾 ∈ Proset → (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})) |
15 | 14 | rneqd 5782 |
. . . . . . 7
⊢ (𝐾 ∈ Proset → ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})) |
16 | | ordtposval.e |
. . . . . . 7
⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) |
17 | 15, 16 | eqtr4di 2792 |
. . . . . 6
⊢ (𝐾 ∈ Proset → ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) = 𝐸) |
18 | 11 | rabeqdv 3387 |
. . . . . . . . 9
⊢ (𝐾 ∈ Proset → {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) |
19 | 11, 18 | mpteq12dv 5116 |
. . . . . . . 8
⊢ (𝐾 ∈ Proset → (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) |
20 | 19 | rneqd 5782 |
. . . . . . 7
⊢ (𝐾 ∈ Proset → ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) |
21 | | ordtposval.f |
. . . . . . 7
⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) |
22 | 20, 21 | eqtr4di 2792 |
. . . . . 6
⊢ (𝐾 ∈ Proset → ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}) = 𝐹) |
23 | 17, 22 | uneq12d 4055 |
. . . . 5
⊢ (𝐾 ∈ Proset → (ran
(𝑥 ∈ dom ≤ ↦
{𝑦 ∈ dom ≤ ∣
¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦})) = (𝐸 ∪ 𝐹)) |
24 | 12, 23 | uneq12d 4055 |
. . . 4
⊢ (𝐾 ∈ Proset → ({dom
≤ }
∪ (ran (𝑥 ∈ dom
≤
↦ {𝑦 ∈ dom ≤ ∣
¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}))) = ({𝐵} ∪ (𝐸 ∪ 𝐹))) |
25 | 24 | fveq2d 6681 |
. . 3
⊢ (𝐾 ∈ Proset →
(fi‘({dom ≤ } ∪ (ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦})))) = (fi‘({𝐵} ∪ (𝐸 ∪ 𝐹)))) |
26 | 25 | fveq2d 6681 |
. 2
⊢ (𝐾 ∈ Proset →
(topGen‘(fi‘({dom ≤ } ∪ (ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}))))) = (topGen‘(fi‘({𝐵} ∪ (𝐸 ∪ 𝐹))))) |
27 | 9, 26 | syl5eq 2786 |
1
⊢ (𝐾 ∈ Proset →
(ordTop‘ ≤ ) =
(topGen‘(fi‘({𝐵} ∪ (𝐸 ∪ 𝐹))))) |