| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ordtNEW.l | . . . . 5
⊢  ≤ =
((le‘𝐾) ∩ (𝐵 × 𝐵)) | 
| 2 |  | fvex 6918 | . . . . . 6
⊢
(le‘𝐾) ∈
V | 
| 3 | 2 | inex1 5316 | . . . . 5
⊢
((le‘𝐾) ∩
(𝐵 × 𝐵)) ∈ V | 
| 4 | 1, 3 | eqeltri 2836 | . . . 4
⊢  ≤ ∈
V | 
| 5 | 4 | inex1 5316 | . . 3
⊢ ( ≤ ∩
(𝐴 × 𝐴)) ∈ V | 
| 6 |  | eqid 2736 | . . . 4
⊢ dom (
≤
∩ (𝐴 × 𝐴)) = dom ( ≤ ∩ (𝐴 × 𝐴)) | 
| 7 |  | eqid 2736 | . . . 4
⊢ ran
(𝑥 ∈ dom ( ≤ ∩
(𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) = ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) | 
| 8 |  | eqid 2736 | . . . 4
⊢ ran
(𝑥 ∈ dom ( ≤ ∩
(𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦}) = ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦}) | 
| 9 | 6, 7, 8 | ordtval 23198 | . . 3
⊢ (( ≤ ∩
(𝐴 × 𝐴)) ∈ V →
(ordTop‘( ≤ ∩ (𝐴 × 𝐴))) = (topGen‘(fi‘({dom ( ≤ ∩
(𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦})))))) | 
| 10 | 5, 9 | mp1i 13 | . 2
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) = (topGen‘(fi‘({dom ( ≤ ∩
(𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦})))))) | 
| 11 |  | ordttop 23209 | . . . . . 6
⊢ ( ≤ ∈ V
→ (ordTop‘ ≤ ) ∈
Top) | 
| 12 | 4, 11 | ax-mp 5 | . . . . 5
⊢
(ordTop‘ ≤ ) ∈
Top | 
| 13 |  | ordtNEW.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝐾) | 
| 14 |  | fvex 6918 | . . . . . . 7
⊢
(Base‘𝐾)
∈ V | 
| 15 | 13, 14 | eqeltri 2836 | . . . . . 6
⊢ 𝐵 ∈ V | 
| 16 | 15 | ssex 5320 | . . . . 5
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) | 
| 17 |  | resttop 23169 | . . . . 5
⊢
(((ordTop‘ ≤ ) ∈ Top ∧
𝐴 ∈ V) →
((ordTop‘ ≤ ) ↾t
𝐴) ∈
Top) | 
| 18 | 12, 16, 17 | sylancr 587 | . . . 4
⊢ (𝐴 ⊆ 𝐵 → ((ordTop‘ ≤ ) ↾t
𝐴) ∈
Top) | 
| 19 | 18 | adantl 481 | . . 3
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ((ordTop‘ ≤ ) ↾t
𝐴) ∈
Top) | 
| 20 | 13 | ressprs 32955 | . . . . . . . . 9
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ Proset ) | 
| 21 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Base‘(𝐾
↾s 𝐴)) =
(Base‘(𝐾
↾s 𝐴)) | 
| 22 |  | eqid 2736 | . . . . . . . . . 10
⊢
((le‘(𝐾
↾s 𝐴))
∩ ((Base‘(𝐾
↾s 𝐴))
× (Base‘(𝐾
↾s 𝐴)))) =
((le‘(𝐾
↾s 𝐴))
∩ ((Base‘(𝐾
↾s 𝐴))
× (Base‘(𝐾
↾s 𝐴)))) | 
| 23 | 21, 22 | prsdm 33914 | . . . . . . . . 9
⊢ ((𝐾 ↾s 𝐴) ∈ Proset → dom
((le‘(𝐾
↾s 𝐴))
∩ ((Base‘(𝐾
↾s 𝐴))
× (Base‘(𝐾
↾s 𝐴)))) =
(Base‘(𝐾
↾s 𝐴))) | 
| 24 | 20, 23 | syl 17 | . . . . . . . 8
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴)))) = (Base‘(𝐾 ↾s 𝐴))) | 
| 25 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (𝐾 ↾s 𝐴) = (𝐾 ↾s 𝐴) | 
| 26 | 25, 13 | ressbas2 17284 | . . . . . . . . . . . . 13
⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘(𝐾 ↾s 𝐴))) | 
| 27 |  | fvex 6918 | . . . . . . . . . . . . 13
⊢
(Base‘(𝐾
↾s 𝐴))
∈ V | 
| 28 | 26, 27 | eqeltrdi 2848 | . . . . . . . . . . . 12
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) | 
| 29 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(le‘𝐾) =
(le‘𝐾) | 
| 30 | 25, 29 | ressle 17425 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ V → (le‘𝐾) = (le‘(𝐾 ↾s 𝐴))) | 
| 31 | 28, 30 | syl 17 | . . . . . . . . . . 11
⊢ (𝐴 ⊆ 𝐵 → (le‘𝐾) = (le‘(𝐾 ↾s 𝐴))) | 
| 32 | 31 | adantl 481 | . . . . . . . . . 10
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (le‘𝐾) = (le‘(𝐾 ↾s 𝐴))) | 
| 33 | 26 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → 𝐴 = (Base‘(𝐾 ↾s 𝐴))) | 
| 34 | 33 | sqxpeqd 5716 | . . . . . . . . . 10
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝐴 × 𝐴) = ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴)))) | 
| 35 | 32, 34 | ineq12d 4220 | . . . . . . . . 9
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ((le‘𝐾) ∩ (𝐴 × 𝐴)) = ((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))) | 
| 36 | 35 | dmeqd 5915 | . . . . . . . 8
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ((le‘𝐾) ∩ (𝐴 × 𝐴)) = dom ((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))) | 
| 37 | 24, 36, 33 | 3eqtr4d 2786 | . . . . . . 7
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ((le‘𝐾) ∩ (𝐴 × 𝐴)) = 𝐴) | 
| 38 | 13, 1 | prsss 33916 | . . . . . . . 8
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘𝐾) ∩ (𝐴 × 𝐴))) | 
| 39 | 38 | dmeqd 5915 | . . . . . . 7
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) = dom ((le‘𝐾) ∩ (𝐴 × 𝐴))) | 
| 40 | 13, 1 | prsdm 33914 | . . . . . . . . . 10
⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵) | 
| 41 | 40 | sseq2d 4015 | . . . . . . . . 9
⊢ (𝐾 ∈ Proset → (𝐴 ⊆ dom ≤ ↔ 𝐴 ⊆ 𝐵)) | 
| 42 | 41 | biimpar 477 | . . . . . . . 8
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → 𝐴 ⊆ dom ≤ ) | 
| 43 |  | sseqin2 4222 | . . . . . . . 8
⊢ (𝐴 ⊆ dom ≤ ↔ (dom ≤ ∩
𝐴) = 𝐴) | 
| 44 | 42, 43 | sylib 218 | . . . . . . 7
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (dom ≤ ∩ 𝐴) = 𝐴) | 
| 45 | 37, 39, 44 | 3eqtr4d 2786 | . . . . . 6
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) = (dom ≤ ∩ 𝐴)) | 
| 46 | 4, 11 | mp1i 13 | . . . . . . 7
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (ordTop‘ ≤ ) ∈
Top) | 
| 47 | 16 | adantl 481 | . . . . . . 7
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → 𝐴 ∈ V) | 
| 48 |  | eqid 2736 | . . . . . . . . . 10
⊢ dom ≤ = dom
≤ | 
| 49 | 48 | ordttopon 23202 | . . . . . . . . 9
⊢ ( ≤ ∈ V
→ (ordTop‘ ≤ ) ∈
(TopOn‘dom ≤ )) | 
| 50 | 4, 49 | mp1i 13 | . . . . . . . 8
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (ordTop‘ ≤ ) ∈
(TopOn‘dom ≤ )) | 
| 51 |  | toponmax 22933 | . . . . . . . 8
⊢
((ordTop‘ ≤ ) ∈
(TopOn‘dom ≤ ) → dom ≤ ∈
(ordTop‘ ≤ )) | 
| 52 | 50, 51 | syl 17 | . . . . . . 7
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ≤ ∈ (ordTop‘
≤
)) | 
| 53 |  | elrestr 17474 | . . . . . . 7
⊢
(((ordTop‘ ≤ ) ∈ Top ∧
𝐴 ∈ V ∧ dom ≤ ∈
(ordTop‘ ≤ )) → (dom ≤ ∩
𝐴) ∈ ((ordTop‘
≤ )
↾t 𝐴)) | 
| 54 | 46, 47, 52, 53 | syl3anc 1372 | . . . . . 6
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (dom ≤ ∩ 𝐴) ∈ ((ordTop‘ ≤ ) ↾t
𝐴)) | 
| 55 | 45, 54 | eqeltrd 2840 | . . . . 5
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) ∈ ((ordTop‘ ≤ ) ↾t
𝐴)) | 
| 56 | 55 | snssd 4808 | . . . 4
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → {dom ( ≤ ∩ (𝐴 × 𝐴))} ⊆ ((ordTop‘ ≤ )
↾t 𝐴)) | 
| 57 |  | rabeq 3450 | . . . . . . . . 9
⊢ (dom (
≤
∩ (𝐴 × 𝐴)) = (dom ≤ ∩ 𝐴) → {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥} = {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) | 
| 58 | 45, 57 | syl 17 | . . . . . . . 8
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥} = {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) | 
| 59 | 45, 58 | mpteq12dv 5232 | . . . . . . 7
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) = (𝑥 ∈ (dom ≤ ∩ 𝐴) ↦ {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥})) | 
| 60 | 59 | rneqd 5948 | . . . . . 6
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) = ran (𝑥 ∈ (dom ≤ ∩ 𝐴) ↦ {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥})) | 
| 61 |  | inrab2 4316 | . . . . . . . . . 10
⊢ ({𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥} ∩ 𝐴) = {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑦 ≤ 𝑥} | 
| 62 |  | inss2 4237 | . . . . . . . . . . . . . 14
⊢ (dom
≤
∩ 𝐴) ⊆ 𝐴 | 
| 63 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) ∧ 𝑦 ∈ (dom ≤ ∩ 𝐴)) → 𝑦 ∈ (dom ≤ ∩ 𝐴)) | 
| 64 | 62, 63 | sselid 3980 | . . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) ∧ 𝑦 ∈ (dom ≤ ∩ 𝐴)) → 𝑦 ∈ 𝐴) | 
| 65 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) → 𝑥 ∈ (dom ≤ ∩ 𝐴)) | 
| 66 | 62, 65 | sselid 3980 | . . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) → 𝑥 ∈ 𝐴) | 
| 67 | 66 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) ∧ 𝑦 ∈ (dom ≤ ∩ 𝐴)) → 𝑥 ∈ 𝐴) | 
| 68 |  | brinxp 5763 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑦 ≤ 𝑥 ↔ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥)) | 
| 69 | 64, 67, 68 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) ∧ 𝑦 ∈ (dom ≤ ∩ 𝐴)) → (𝑦 ≤ 𝑥 ↔ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥)) | 
| 70 | 69 | notbid 318 | . . . . . . . . . . 11
⊢ ((((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) ∧ 𝑦 ∈ (dom ≤ ∩ 𝐴)) → (¬ 𝑦 ≤ 𝑥 ↔ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥)) | 
| 71 | 70 | rabbidva 3442 | . . . . . . . . . 10
⊢ (((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) → {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑦 ≤ 𝑥} = {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) | 
| 72 | 61, 71 | eqtrid 2788 | . . . . . . . . 9
⊢ (((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) → ({𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥} ∩ 𝐴) = {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) | 
| 73 | 4, 11 | mp1i 13 | . . . . . . . . . 10
⊢ (((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) → (ordTop‘ ≤ ) ∈
Top) | 
| 74 | 47 | adantr 480 | . . . . . . . . . 10
⊢ (((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) → 𝐴 ∈ V) | 
| 75 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → 𝐾 ∈ Proset ) | 
| 76 |  | inss1 4236 | . . . . . . . . . . . 12
⊢ (dom
≤
∩ 𝐴) ⊆ dom ≤ | 
| 77 | 76 | sseli 3978 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (dom ≤ ∩ 𝐴) → 𝑥 ∈ dom ≤ ) | 
| 78 | 48 | ordtopn1 23203 | . . . . . . . . . . . . 13
⊢ (( ≤ ∈ V
∧ 𝑥 ∈ dom ≤ ) →
{𝑦 ∈ dom ≤ ∣
¬ 𝑦 ≤ 𝑥} ∈ (ordTop‘ ≤ )) | 
| 79 | 4, 78 | mpan 690 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ dom ≤ → {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥} ∈ (ordTop‘ ≤ )) | 
| 80 | 79 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ Proset ∧ 𝑥 ∈ dom ≤ ) → {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥} ∈ (ordTop‘ ≤ )) | 
| 81 | 75, 77, 80 | syl2an 596 | . . . . . . . . . 10
⊢ (((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) → {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥} ∈ (ordTop‘ ≤ )) | 
| 82 |  | elrestr 17474 | . . . . . . . . . 10
⊢
(((ordTop‘ ≤ ) ∈ Top ∧
𝐴 ∈ V ∧ {𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥} ∈ (ordTop‘ ≤ )) → ({𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥} ∩ 𝐴) ∈ ((ordTop‘ ≤ ) ↾t
𝐴)) | 
| 83 | 73, 74, 81, 82 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) → ({𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥} ∩ 𝐴) ∈ ((ordTop‘ ≤ ) ↾t
𝐴)) | 
| 84 | 72, 83 | eqeltrrd 2841 | . . . . . . . 8
⊢ (((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) → {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥} ∈ ((ordTop‘ ≤ ) ↾t
𝐴)) | 
| 85 | 84 | fmpttd 7134 | . . . . . . 7
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝑥 ∈ (dom ≤ ∩ 𝐴) ↦ {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}):(dom ≤ ∩ 𝐴)⟶((ordTop‘ ≤ ) ↾t
𝐴)) | 
| 86 | 85 | frnd 6743 | . . . . . 6
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ran (𝑥 ∈ (dom ≤ ∩ 𝐴) ↦ {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) ⊆ ((ordTop‘ ≤ ) ↾t
𝐴)) | 
| 87 | 60, 86 | eqsstrd 4017 | . . . . 5
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) ⊆ ((ordTop‘ ≤ ) ↾t
𝐴)) | 
| 88 |  | rabeq 3450 | . . . . . . . . 9
⊢ (dom (
≤
∩ (𝐴 × 𝐴)) = (dom ≤ ∩ 𝐴) → {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦} = {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦}) | 
| 89 | 45, 88 | syl 17 | . . . . . . . 8
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦} = {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦}) | 
| 90 | 45, 89 | mpteq12dv 5232 | . . . . . . 7
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦}) = (𝑥 ∈ (dom ≤ ∩ 𝐴) ↦ {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦})) | 
| 91 | 90 | rneqd 5948 | . . . . . 6
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦}) = ran (𝑥 ∈ (dom ≤ ∩ 𝐴) ↦ {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦})) | 
| 92 |  | inrab2 4316 | . . . . . . . . . 10
⊢ ({𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦} ∩ 𝐴) = {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑥 ≤ 𝑦} | 
| 93 |  | brinxp 5763 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≤ 𝑦 ↔ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦)) | 
| 94 | 67, 64, 93 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) ∧ 𝑦 ∈ (dom ≤ ∩ 𝐴)) → (𝑥 ≤ 𝑦 ↔ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦)) | 
| 95 | 94 | notbid 318 | . . . . . . . . . . 11
⊢ ((((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) ∧ 𝑦 ∈ (dom ≤ ∩ 𝐴)) → (¬ 𝑥 ≤ 𝑦 ↔ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦)) | 
| 96 | 95 | rabbidva 3442 | . . . . . . . . . 10
⊢ (((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) → {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑥 ≤ 𝑦} = {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦}) | 
| 97 | 92, 96 | eqtrid 2788 | . . . . . . . . 9
⊢ (((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) → ({𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦} ∩ 𝐴) = {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦}) | 
| 98 | 48 | ordtopn2 23204 | . . . . . . . . . . . . 13
⊢ (( ≤ ∈ V
∧ 𝑥 ∈ dom ≤ ) →
{𝑦 ∈ dom ≤ ∣
¬ 𝑥 ≤ 𝑦} ∈ (ordTop‘ ≤ )) | 
| 99 | 4, 98 | mpan 690 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ dom ≤ → {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦} ∈ (ordTop‘ ≤ )) | 
| 100 | 99 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ Proset ∧ 𝑥 ∈ dom ≤ ) → {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦} ∈ (ordTop‘ ≤ )) | 
| 101 | 75, 77, 100 | syl2an 596 | . . . . . . . . . 10
⊢ (((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) → {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦} ∈ (ordTop‘ ≤ )) | 
| 102 |  | elrestr 17474 | . . . . . . . . . 10
⊢
(((ordTop‘ ≤ ) ∈ Top ∧
𝐴 ∈ V ∧ {𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦} ∈ (ordTop‘ ≤ )) → ({𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦} ∩ 𝐴) ∈ ((ordTop‘ ≤ ) ↾t
𝐴)) | 
| 103 | 73, 74, 101, 102 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) → ({𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦} ∩ 𝐴) ∈ ((ordTop‘ ≤ ) ↾t
𝐴)) | 
| 104 | 97, 103 | eqeltrrd 2841 | . . . . . . . 8
⊢ (((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ (dom ≤ ∩ 𝐴)) → {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦} ∈ ((ordTop‘ ≤ ) ↾t
𝐴)) | 
| 105 | 104 | fmpttd 7134 | . . . . . . 7
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝑥 ∈ (dom ≤ ∩ 𝐴) ↦ {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦}):(dom ≤ ∩ 𝐴)⟶((ordTop‘ ≤ ) ↾t
𝐴)) | 
| 106 | 105 | frnd 6743 | . . . . . 6
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ran (𝑥 ∈ (dom ≤ ∩ 𝐴) ↦ {𝑦 ∈ (dom ≤ ∩ 𝐴) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦}) ⊆ ((ordTop‘ ≤ ) ↾t
𝐴)) | 
| 107 | 91, 106 | eqsstrd 4017 | . . . . 5
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦}) ⊆ ((ordTop‘ ≤ ) ↾t
𝐴)) | 
| 108 | 87, 107 | unssd 4191 | . . . 4
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦})) ⊆ ((ordTop‘ ≤ )
↾t 𝐴)) | 
| 109 | 56, 108 | unssd 4191 | . . 3
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ({dom ( ≤ ∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦}))) ⊆ ((ordTop‘ ≤ )
↾t 𝐴)) | 
| 110 |  | tgfiss 22999 | . . 3
⊢
((((ordTop‘ ≤ ) ↾t
𝐴) ∈ Top ∧ ({dom (
≤
∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦}))) ⊆ ((ordTop‘ ≤ )
↾t 𝐴))
→ (topGen‘(fi‘({dom ( ≤ ∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦}))))) ⊆ ((ordTop‘ ≤ )
↾t 𝐴)) | 
| 111 | 19, 109, 110 | syl2anc 584 | . 2
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (topGen‘(fi‘({dom (
≤
∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦( ≤ ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥( ≤ ∩ (𝐴 × 𝐴))𝑦}))))) ⊆ ((ordTop‘ ≤ )
↾t 𝐴)) | 
| 112 | 10, 111 | eqsstrd 4017 | 1
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘ ≤ )
↾t 𝐴)) |