| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ordtrest2.2 | . . . 4
⊢ (𝜑 → 𝑅 ∈ TosetRel ) | 
| 2 |  | tsrps 18632 | . . . 4
⊢ (𝑅 ∈ TosetRel → 𝑅 ∈
PosetRel) | 
| 3 | 1, 2 | syl 17 | . . 3
⊢ (𝜑 → 𝑅 ∈ PosetRel) | 
| 4 |  | ordtrest2.1 | . . . . 5
⊢ 𝑋 = dom 𝑅 | 
| 5 | 1 | dmexd 7925 | . . . . 5
⊢ (𝜑 → dom 𝑅 ∈ V) | 
| 6 | 4, 5 | eqeltrid 2845 | . . . 4
⊢ (𝜑 → 𝑋 ∈ V) | 
| 7 |  | ordtrest2.3 | . . . 4
⊢ (𝜑 → 𝐴 ⊆ 𝑋) | 
| 8 | 6, 7 | ssexd 5324 | . . 3
⊢ (𝜑 → 𝐴 ∈ V) | 
| 9 |  | ordtrest 23210 | . . 3
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ V) →
(ordTop‘(𝑅 ∩
(𝐴 × 𝐴))) ⊆ ((ordTop‘𝑅) ↾t 𝐴)) | 
| 10 | 3, 8, 9 | syl2anc 584 | . 2
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘𝑅) ↾t 𝐴)) | 
| 11 |  | eqid 2737 | . . . . . . . 8
⊢ ran
(𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) = ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) | 
| 12 |  | eqid 2737 | . . . . . . . 8
⊢ ran
(𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}) = ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}) | 
| 13 | 4, 11, 12 | ordtval 23197 | . . . . . . 7
⊢ (𝑅 ∈ TosetRel →
(ordTop‘𝑅) =
(topGen‘(fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))))) | 
| 14 | 1, 13 | syl 17 | . . . . . 6
⊢ (𝜑 → (ordTop‘𝑅) =
(topGen‘(fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))))) | 
| 15 | 14 | oveq1d 7446 | . . . . 5
⊢ (𝜑 → ((ordTop‘𝑅) ↾t 𝐴) =
((topGen‘(fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))))) ↾t 𝐴)) | 
| 16 |  | fibas 22984 | . . . . . 6
⊢
(fi‘({𝑋} ∪
(ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ∈ TopBases | 
| 17 |  | tgrest 23167 | . . . . . 6
⊢
(((fi‘({𝑋}
∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ∈ TopBases ∧ 𝐴 ∈ V) →
(topGen‘((fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ↾t 𝐴)) = ((topGen‘(fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))))) ↾t 𝐴)) | 
| 18 | 16, 8, 17 | sylancr 587 | . . . . 5
⊢ (𝜑 →
(topGen‘((fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ↾t 𝐴)) = ((topGen‘(fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))))) ↾t 𝐴)) | 
| 19 | 15, 18 | eqtr4d 2780 | . . . 4
⊢ (𝜑 → ((ordTop‘𝑅) ↾t 𝐴) =
(topGen‘((fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ↾t 𝐴))) | 
| 20 |  | firest 17477 | . . . . 5
⊢
(fi‘(({𝑋}
∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴)) = ((fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ↾t 𝐴) | 
| 21 | 20 | fveq2i 6909 | . . . 4
⊢
(topGen‘(fi‘(({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴))) = (topGen‘((fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ↾t 𝐴)) | 
| 22 | 19, 21 | eqtr4di 2795 | . . 3
⊢ (𝜑 → ((ordTop‘𝑅) ↾t 𝐴) =
(topGen‘(fi‘(({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴)))) | 
| 23 |  | inex1g 5319 | . . . . . 6
⊢ (𝑅 ∈ TosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V) | 
| 24 | 1, 23 | syl 17 | . . . . 5
⊢ (𝜑 → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V) | 
| 25 |  | ordttop 23208 | . . . . 5
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∈ Top) | 
| 26 | 24, 25 | syl 17 | . . . 4
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∈ Top) | 
| 27 | 4, 11, 12 | ordtuni 23198 | . . . . . . . . 9
⊢ (𝑅 ∈ TosetRel → 𝑋 = ∪
({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) | 
| 28 | 1, 27 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑋 = ∪ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) | 
| 29 | 28, 6 | eqeltrrd 2842 | . . . . . . 7
⊢ (𝜑 → ∪ ({𝑋}
∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ∈ V) | 
| 30 |  | uniexb 7784 | . . . . . . 7
⊢ (({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ∈ V ↔ ∪ ({𝑋}
∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ∈ V) | 
| 31 | 29, 30 | sylibr 234 | . . . . . 6
⊢ (𝜑 → ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ∈ V) | 
| 32 |  | restval 17471 | . . . . . 6
⊢ ((({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ∈ V ∧ 𝐴 ∈ V) → (({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴) = ran (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴))) | 
| 33 | 31, 8, 32 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴) = ran (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴))) | 
| 34 |  | sseqin2 4223 | . . . . . . . . . . . 12
⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴) | 
| 35 | 7, 34 | sylib 218 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ∩ 𝐴) = 𝐴) | 
| 36 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢ dom
(𝑅 ∩ (𝐴 × 𝐴)) = dom (𝑅 ∩ (𝐴 × 𝐴)) | 
| 37 | 36 | ordttopon 23201 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∈ (TopOn‘dom (𝑅 ∩ (𝐴 × 𝐴)))) | 
| 38 | 24, 37 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∈ (TopOn‘dom (𝑅 ∩ (𝐴 × 𝐴)))) | 
| 39 | 4 | psssdm 18627 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ⊆ 𝑋) → dom (𝑅 ∩ (𝐴 × 𝐴)) = 𝐴) | 
| 40 | 3, 7, 39 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑅 ∩ (𝐴 × 𝐴)) = 𝐴) | 
| 41 | 40 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ (𝜑 → (TopOn‘dom (𝑅 ∩ (𝐴 × 𝐴))) = (TopOn‘𝐴)) | 
| 42 | 38, 41 | eleqtrd 2843 | . . . . . . . . . . . 12
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∈ (TopOn‘𝐴)) | 
| 43 |  | toponmax 22932 | . . . . . . . . . . . 12
⊢
((ordTop‘(𝑅
∩ (𝐴 × 𝐴))) ∈ (TopOn‘𝐴) → 𝐴 ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 44 | 42, 43 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 45 | 35, 44 | eqeltrd 2841 | . . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 46 |  | elsni 4643 | . . . . . . . . . . . 12
⊢ (𝑣 ∈ {𝑋} → 𝑣 = 𝑋) | 
| 47 | 46 | ineq1d 4219 | . . . . . . . . . . 11
⊢ (𝑣 ∈ {𝑋} → (𝑣 ∩ 𝐴) = (𝑋 ∩ 𝐴)) | 
| 48 | 47 | eleq1d 2826 | . . . . . . . . . 10
⊢ (𝑣 ∈ {𝑋} → ((𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ (𝑋 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))))) | 
| 49 | 45, 48 | syl5ibrcom 247 | . . . . . . . . 9
⊢ (𝜑 → (𝑣 ∈ {𝑋} → (𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))))) | 
| 50 | 49 | ralrimiv 3145 | . . . . . . . 8
⊢ (𝜑 → ∀𝑣 ∈ {𝑋} (𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 51 |  | ordtrest2.4 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} ⊆ 𝐴) | 
| 52 | 4, 1, 7, 51 | ordtrest2lem 23211 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 53 |  | df-rn 5696 | . . . . . . . . . . 11
⊢ ran 𝑅 = dom ◡𝑅 | 
| 54 |  | cnvtsr 18633 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ TosetRel → ◡𝑅 ∈ TosetRel ) | 
| 55 | 1, 54 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → ◡𝑅 ∈ TosetRel ) | 
| 56 | 4 | psrn 18620 | . . . . . . . . . . . . 13
⊢ (𝑅 ∈ PosetRel → 𝑋 = ran 𝑅) | 
| 57 | 3, 56 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 = ran 𝑅) | 
| 58 | 7, 57 | sseqtrd 4020 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ ran 𝑅) | 
| 59 | 57 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑋 = ran 𝑅) | 
| 60 | 59 | rabeqdv 3452 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} = {𝑧 ∈ ran 𝑅 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)}) | 
| 61 |  | vex 3484 | . . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V | 
| 62 |  | vex 3484 | . . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V | 
| 63 | 61, 62 | brcnv 5893 | . . . . . . . . . . . . . . . 16
⊢ (𝑦◡𝑅𝑧 ↔ 𝑧𝑅𝑦) | 
| 64 |  | vex 3484 | . . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V | 
| 65 | 62, 64 | brcnv 5893 | . . . . . . . . . . . . . . . 16
⊢ (𝑧◡𝑅𝑥 ↔ 𝑥𝑅𝑧) | 
| 66 | 63, 65 | anbi12ci 629 | . . . . . . . . . . . . . . 15
⊢ ((𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥) ↔ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)) | 
| 67 | 66 | rabbii 3442 | . . . . . . . . . . . . . 14
⊢ {𝑧 ∈ ran 𝑅 ∣ (𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥)} = {𝑧 ∈ ran 𝑅 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} | 
| 68 | 60, 67 | eqtr4di 2795 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} = {𝑧 ∈ ran 𝑅 ∣ (𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥)}) | 
| 69 | 68, 51 | eqsstrrd 4019 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ ran 𝑅 ∣ (𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥)} ⊆ 𝐴) | 
| 70 | 69 | ancom2s 650 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → {𝑧 ∈ ran 𝑅 ∣ (𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥)} ⊆ 𝐴) | 
| 71 | 53, 55, 58, 70 | ordtrest2lem 23211 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ ran 𝑅 ↦ {𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤◡𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(◡𝑅 ∩ (𝐴 × 𝐴)))) | 
| 72 |  | vex 3484 | . . . . . . . . . . . . . . . . . 18
⊢ 𝑤 ∈ V | 
| 73 | 72, 62 | brcnv 5893 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤◡𝑅𝑧 ↔ 𝑧𝑅𝑤) | 
| 74 | 73 | bicomi 224 | . . . . . . . . . . . . . . . 16
⊢ (𝑧𝑅𝑤 ↔ 𝑤◡𝑅𝑧) | 
| 75 | 74 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑧𝑅𝑤 ↔ 𝑤◡𝑅𝑧)) | 
| 76 | 75 | notbid 318 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (¬ 𝑧𝑅𝑤 ↔ ¬ 𝑤◡𝑅𝑧)) | 
| 77 | 57, 76 | rabeqbidv 3455 | . . . . . . . . . . . . 13
⊢ (𝜑 → {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤} = {𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤◡𝑅𝑧}) | 
| 78 | 57, 77 | mpteq12dv 5233 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}) = (𝑧 ∈ ran 𝑅 ↦ {𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤◡𝑅𝑧})) | 
| 79 | 78 | rneqd 5949 | . . . . . . . . . . 11
⊢ (𝜑 → ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}) = ran (𝑧 ∈ ran 𝑅 ↦ {𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤◡𝑅𝑧})) | 
| 80 |  | psss 18625 | . . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel) | 
| 81 | 3, 80 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel) | 
| 82 |  | ordtcnv 23209 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel →
(ordTop‘◡(𝑅 ∩ (𝐴 × 𝐴))) = (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 83 | 81, 82 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (ordTop‘◡(𝑅 ∩ (𝐴 × 𝐴))) = (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 84 |  | cnvin 6164 | . . . . . . . . . . . . . . 15
⊢ ◡(𝑅 ∩ (𝐴 × 𝐴)) = (◡𝑅 ∩ ◡(𝐴 × 𝐴)) | 
| 85 |  | cnvxp 6177 | . . . . . . . . . . . . . . . 16
⊢ ◡(𝐴 × 𝐴) = (𝐴 × 𝐴) | 
| 86 | 85 | ineq2i 4217 | . . . . . . . . . . . . . . 15
⊢ (◡𝑅 ∩ ◡(𝐴 × 𝐴)) = (◡𝑅 ∩ (𝐴 × 𝐴)) | 
| 87 | 84, 86 | eqtri 2765 | . . . . . . . . . . . . . 14
⊢ ◡(𝑅 ∩ (𝐴 × 𝐴)) = (◡𝑅 ∩ (𝐴 × 𝐴)) | 
| 88 | 87 | fveq2i 6909 | . . . . . . . . . . . . 13
⊢
(ordTop‘◡(𝑅 ∩ (𝐴 × 𝐴))) = (ordTop‘(◡𝑅 ∩ (𝐴 × 𝐴))) | 
| 89 | 83, 88 | eqtr3di 2792 | . . . . . . . . . . . 12
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) = (ordTop‘(◡𝑅 ∩ (𝐴 × 𝐴)))) | 
| 90 | 89 | eleq2d 2827 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ (𝑣 ∩ 𝐴) ∈ (ordTop‘(◡𝑅 ∩ (𝐴 × 𝐴))))) | 
| 91 | 79, 90 | raleqbidv 3346 | . . . . . . . . . 10
⊢ (𝜑 → (∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ ∀𝑣 ∈ ran (𝑧 ∈ ran 𝑅 ↦ {𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤◡𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(◡𝑅 ∩ (𝐴 × 𝐴))))) | 
| 92 | 71, 91 | mpbird 257 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 93 |  | ralunb 4197 | . . . . . . . . 9
⊢
(∀𝑣 ∈
(ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ (∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∧ ∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))))) | 
| 94 | 52, 92, 93 | sylanbrc 583 | . . . . . . . 8
⊢ (𝜑 → ∀𝑣 ∈ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 95 |  | ralunb 4197 | . . . . . . . 8
⊢
(∀𝑣 ∈
({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ (∀𝑣 ∈ {𝑋} (𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∧ ∀𝑣 ∈ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))))) | 
| 96 | 50, 94, 95 | sylanbrc 583 | . . . . . . 7
⊢ (𝜑 → ∀𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 97 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)) = (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)) | 
| 98 | 97 | fmpt 7130 | . . . . . . 7
⊢
(∀𝑣 ∈
({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)):({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))⟶(ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 99 | 96, 98 | sylib 218 | . . . . . 6
⊢ (𝜑 → (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)):({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))⟶(ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 100 | 99 | frnd 6744 | . . . . 5
⊢ (𝜑 → ran (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 101 | 33, 100 | eqsstrd 4018 | . . . 4
⊢ (𝜑 → (({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 102 |  | tgfiss 22998 | . . . 4
⊢
(((ordTop‘(𝑅
∩ (𝐴 × 𝐴))) ∈ Top ∧ (({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) → (topGen‘(fi‘(({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴))) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 103 | 26, 101, 102 | syl2anc 584 | . . 3
⊢ (𝜑 →
(topGen‘(fi‘(({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴))) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 104 | 22, 103 | eqsstrd 4018 | . 2
⊢ (𝜑 → ((ordTop‘𝑅) ↾t 𝐴) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | 
| 105 | 10, 104 | eqssd 4001 | 1
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) = ((ordTop‘𝑅) ↾t 𝐴)) |