Proof of Theorem ordtprsval
Step | Hyp | Ref
| Expression |
1 | | ordtNEW.l |
. . . 4
⊢ ≤ =
((le‘𝐾) ∩ (𝐵 × 𝐵)) |
2 | | fvex 6113 |
. . . . 5
⊢
(le‘𝐾) ∈
V |
3 | 2 | inex1 4727 |
. . . 4
⊢
((le‘𝐾) ∩
(𝐵 × 𝐵)) ∈ V |
4 | 1, 3 | eqeltri 2684 |
. . 3
⊢ ≤ ∈
V |
5 | | eqid 2610 |
. . . 4
⊢ dom ≤ = dom
≤ |
6 | | eqid 2610 |
. . . 4
⊢ ran
(𝑥 ∈ dom ≤ ↦
{𝑦 ∈ dom ≤ ∣
¬ 𝑦 ≤ 𝑥}) = ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) |
7 | | eqid 2610 |
. . . 4
⊢ ran
(𝑥 ∈ dom ≤ ↦
{𝑦 ∈ dom ≤ ∣
¬ 𝑥 ≤ 𝑦}) = ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}) |
8 | 5, 6, 7 | ordtval 20803 |
. . 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 29288 |
. . . . . 6
⊢ (𝐾 ∈ Preset → dom ≤ = 𝐵) |
12 | 11 | sneqd 4137 |
. . . . 5
⊢ (𝐾 ∈ Preset → {dom ≤ } = {𝐵}) |
13 | | rabeq 3166 |
. . . . . . . . . 10
⊢ (dom
≤ =
𝐵 → {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) |
14 | 11, 13 | syl 17 |
. . . . . . . . 9
⊢ (𝐾 ∈ Preset → {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) |
15 | 11, 14 | mpteq12dv 4663 |
. . . . . . . 8
⊢ (𝐾 ∈ Preset → (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})) |
16 | 15 | rneqd 5274 |
. . . . . . 7
⊢ (𝐾 ∈ Preset → ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})) |
17 | | ordtposval.e |
. . . . . . 7
⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) |
18 | 16, 17 | syl6eqr 2662 |
. . . . . 6
⊢ (𝐾 ∈ Preset → ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) = 𝐸) |
19 | | rabeq 3166 |
. . . . . . . . . 10
⊢ (dom
≤ =
𝐵 → {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) |
20 | 11, 19 | syl 17 |
. . . . . . . . 9
⊢ (𝐾 ∈ Preset → {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) |
21 | 11, 20 | mpteq12dv 4663 |
. . . . . . . 8
⊢ (𝐾 ∈ Preset → (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) |
22 | 21 | rneqd 5274 |
. . . . . . 7
⊢ (𝐾 ∈ Preset → ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) |
23 | | ordtposval.f |
. . . . . . 7
⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) |
24 | 22, 23 | syl6eqr 2662 |
. . . . . 6
⊢ (𝐾 ∈ Preset → ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}) = 𝐹) |
25 | 18, 24 | uneq12d 3730 |
. . . . 5
⊢ (𝐾 ∈ Preset → (ran
(𝑥 ∈ dom ≤ ↦
{𝑦 ∈ dom ≤ ∣
¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦})) = (𝐸 ∪ 𝐹)) |
26 | 12, 25 | uneq12d 3730 |
. . . 4
⊢ (𝐾 ∈ Preset → ({dom
≤ }
∪ (ran (𝑥 ∈ dom
≤
↦ {𝑦 ∈ dom ≤ ∣
¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}))) = ({𝐵} ∪ (𝐸 ∪ 𝐹))) |
27 | 26 | fveq2d 6107 |
. . 3
⊢ (𝐾 ∈ Preset →
(fi‘({dom ≤ } ∪ (ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦})))) = (fi‘({𝐵} ∪ (𝐸 ∪ 𝐹)))) |
28 | 27 | fveq2d 6107 |
. 2
⊢ (𝐾 ∈ Preset →
(topGen‘(fi‘({dom ≤ } ∪ (ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ dom ≤ ↦ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦}))))) = (topGen‘(fi‘({𝐵} ∪ (𝐸 ∪ 𝐹))))) |
29 | 9, 28 | syl5eq 2656 |
1
⊢ (𝐾 ∈ Preset →
(ordTop‘ ≤ ) =
(topGen‘(fi‘({𝐵} ∪ (𝐸 ∪ 𝐹))))) |