| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | qtoprest.2 | . . . . . 6
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | 
| 2 |  | qtoprest.3 | . . . . . . 7
⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) | 
| 3 |  | fofn 6821 | . . . . . . 7
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹 Fn 𝑋) | 
| 4 | 2, 3 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐹 Fn 𝑋) | 
| 5 |  | qtopid 23714 | . . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) | 
| 6 | 1, 4, 5 | syl2anc 584 | . . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) | 
| 7 |  | qtoprest.5 | . . . . . . 7
⊢ (𝜑 → 𝐴 = (◡𝐹 “ 𝑈)) | 
| 8 |  | cnvimass 6099 | . . . . . . . 8
⊢ (◡𝐹 “ 𝑈) ⊆ dom 𝐹 | 
| 9 | 4 | fndmd 6672 | . . . . . . . 8
⊢ (𝜑 → dom 𝐹 = 𝑋) | 
| 10 | 8, 9 | sseqtrid 4025 | . . . . . . 7
⊢ (𝜑 → (◡𝐹 “ 𝑈) ⊆ 𝑋) | 
| 11 | 7, 10 | eqsstrd 4017 | . . . . . 6
⊢ (𝜑 → 𝐴 ⊆ 𝑋) | 
| 12 |  | toponuni 22921 | . . . . . . 7
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) | 
| 13 | 1, 12 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑋 = ∪ 𝐽) | 
| 14 | 11, 13 | sseqtrd 4019 | . . . . 5
⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐽) | 
| 15 |  | eqid 2736 | . . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 16 | 15 | cnrest 23294 | . . . . 5
⊢ ((𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)) ∧ 𝐴 ⊆ ∪ 𝐽) → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn (𝐽 qTop 𝐹))) | 
| 17 | 6, 14, 16 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn (𝐽 qTop 𝐹))) | 
| 18 |  | qtoptopon 23713 | . . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) | 
| 19 | 1, 2, 18 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) | 
| 20 |  | df-ima 5697 | . . . . . . 7
⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴) | 
| 21 | 7 | imaeq2d 6077 | . . . . . . . 8
⊢ (𝜑 → (𝐹 “ 𝐴) = (𝐹 “ (◡𝐹 “ 𝑈))) | 
| 22 |  | qtoprest.4 | . . . . . . . . 9
⊢ (𝜑 → 𝑈 ⊆ 𝑌) | 
| 23 |  | foimacnv 6864 | . . . . . . . . 9
⊢ ((𝐹:𝑋–onto→𝑌 ∧ 𝑈 ⊆ 𝑌) → (𝐹 “ (◡𝐹 “ 𝑈)) = 𝑈) | 
| 24 | 2, 22, 23 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐹 “ (◡𝐹 “ 𝑈)) = 𝑈) | 
| 25 | 21, 24 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → (𝐹 “ 𝐴) = 𝑈) | 
| 26 | 20, 25 | eqtr3id 2790 | . . . . . 6
⊢ (𝜑 → ran (𝐹 ↾ 𝐴) = 𝑈) | 
| 27 |  | eqimss 4041 | . . . . . 6
⊢ (ran
(𝐹 ↾ 𝐴) = 𝑈 → ran (𝐹 ↾ 𝐴) ⊆ 𝑈) | 
| 28 | 26, 27 | syl 17 | . . . . 5
⊢ (𝜑 → ran (𝐹 ↾ 𝐴) ⊆ 𝑈) | 
| 29 |  | cnrest2 23295 | . . . . 5
⊢ (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ ran (𝐹 ↾ 𝐴) ⊆ 𝑈 ∧ 𝑈 ⊆ 𝑌) → ((𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn (𝐽 qTop 𝐹)) ↔ (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈)))) | 
| 30 | 19, 28, 22, 29 | syl3anc 1372 | . . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn (𝐽 qTop 𝐹)) ↔ (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈)))) | 
| 31 | 17, 30 | mpbid 232 | . . 3
⊢ (𝜑 → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈))) | 
| 32 |  | resttopon 23170 | . . . 4
⊢ (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝑈 ⊆ 𝑌) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈)) | 
| 33 | 19, 22, 32 | syl2anc 584 | . . 3
⊢ (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈)) | 
| 34 |  | qtopss 23724 | . . 3
⊢ (((𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈)) ∧ ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈) ∧ ran (𝐹 ↾ 𝐴) = 𝑈) → ((𝐽 qTop 𝐹) ↾t 𝑈) ⊆ ((𝐽 ↾t 𝐴) qTop (𝐹 ↾ 𝐴))) | 
| 35 | 31, 33, 26, 34 | syl3anc 1372 | . 2
⊢ (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) ⊆ ((𝐽 ↾t 𝐴) qTop (𝐹 ↾ 𝐴))) | 
| 36 |  | resttopon 23170 | . . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴)) | 
| 37 | 1, 11, 36 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴)) | 
| 38 |  | fnfun 6667 | . . . . . . . 8
⊢ (𝐹 Fn 𝑋 → Fun 𝐹) | 
| 39 | 4, 38 | syl 17 | . . . . . . 7
⊢ (𝜑 → Fun 𝐹) | 
| 40 | 11, 9 | sseqtrrd 4020 | . . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ dom 𝐹) | 
| 41 |  | fores 6829 | . . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴)) | 
| 42 | 39, 40, 41 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴)) | 
| 43 |  | foeq3 6817 | . . . . . . 7
⊢ ((𝐹 “ 𝐴) = 𝑈 → ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ (𝐹 ↾ 𝐴):𝐴–onto→𝑈)) | 
| 44 | 25, 43 | syl 17 | . . . . . 6
⊢ (𝜑 → ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ (𝐹 ↾ 𝐴):𝐴–onto→𝑈)) | 
| 45 | 42, 44 | mpbid 232 | . . . . 5
⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴–onto→𝑈) | 
| 46 |  | elqtop3 23712 | . . . . 5
⊢ (((𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴) ∧ (𝐹 ↾ 𝐴):𝐴–onto→𝑈) → (𝑥 ∈ ((𝐽 ↾t 𝐴) qTop (𝐹 ↾ 𝐴)) ↔ (𝑥 ⊆ 𝑈 ∧ (◡(𝐹 ↾ 𝐴) “ 𝑥) ∈ (𝐽 ↾t 𝐴)))) | 
| 47 | 37, 45, 46 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝑥 ∈ ((𝐽 ↾t 𝐴) qTop (𝐹 ↾ 𝐴)) ↔ (𝑥 ⊆ 𝑈 ∧ (◡(𝐹 ↾ 𝐴) “ 𝑥) ∈ (𝐽 ↾t 𝐴)))) | 
| 48 |  | cnvresima 6249 | . . . . . . . 8
⊢ (◡(𝐹 ↾ 𝐴) “ 𝑥) = ((◡𝐹 “ 𝑥) ∩ 𝐴) | 
| 49 |  | imass2 6119 | . . . . . . . . . . 11
⊢ (𝑥 ⊆ 𝑈 → (◡𝐹 “ 𝑥) ⊆ (◡𝐹 “ 𝑈)) | 
| 50 | 49 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑈) → (◡𝐹 “ 𝑥) ⊆ (◡𝐹 “ 𝑈)) | 
| 51 | 7 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑈) → 𝐴 = (◡𝐹 “ 𝑈)) | 
| 52 | 50, 51 | sseqtrrd 4020 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑈) → (◡𝐹 “ 𝑥) ⊆ 𝐴) | 
| 53 |  | dfss2 3968 | . . . . . . . . 9
⊢ ((◡𝐹 “ 𝑥) ⊆ 𝐴 ↔ ((◡𝐹 “ 𝑥) ∩ 𝐴) = (◡𝐹 “ 𝑥)) | 
| 54 | 52, 53 | sylib 218 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑈) → ((◡𝐹 “ 𝑥) ∩ 𝐴) = (◡𝐹 “ 𝑥)) | 
| 55 | 48, 54 | eqtrid 2788 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑈) → (◡(𝐹 ↾ 𝐴) “ 𝑥) = (◡𝐹 “ 𝑥)) | 
| 56 | 55 | eleq1d 2825 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑈) → ((◡(𝐹 ↾ 𝐴) “ 𝑥) ∈ (𝐽 ↾t 𝐴) ↔ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) | 
| 57 |  | simplrl 776 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ 𝐽) → 𝑥 ⊆ 𝑈) | 
| 58 |  | dfss2 3968 | . . . . . . . . . 10
⊢ (𝑥 ⊆ 𝑈 ↔ (𝑥 ∩ 𝑈) = 𝑥) | 
| 59 | 57, 58 | sylib 218 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ 𝐽) → (𝑥 ∩ 𝑈) = 𝑥) | 
| 60 |  | topontop 22920 | . . . . . . . . . . . 12
⊢ ((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) → (𝐽 qTop 𝐹) ∈ Top) | 
| 61 | 19, 60 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Top) | 
| 62 | 61 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ 𝐽) → (𝐽 qTop 𝐹) ∈ Top) | 
| 63 |  | toponmax 22933 | . . . . . . . . . . . . . 14
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) | 
| 64 | 1, 63 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ 𝐽) | 
| 65 |  | focdmex 7981 | . . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝐽 → (𝐹:𝑋–onto→𝑌 → 𝑌 ∈ V)) | 
| 66 | 64, 2, 65 | sylc 65 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ V) | 
| 67 | 66, 22 | ssexd 5323 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ V) | 
| 68 | 67 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ 𝐽) → 𝑈 ∈ V) | 
| 69 | 22 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ 𝐽) → 𝑈 ⊆ 𝑌) | 
| 70 | 57, 69 | sstrd 3993 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ 𝐽) → 𝑥 ⊆ 𝑌) | 
| 71 |  | topontop 22920 | . . . . . . . . . . . . . . . 16
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) | 
| 72 | 1, 71 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐽 ∈ Top) | 
| 73 |  | restopn2 23186 | . . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → ((◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴) ↔ ((◡𝐹 “ 𝑥) ∈ 𝐽 ∧ (◡𝐹 “ 𝑥) ⊆ 𝐴))) | 
| 74 | 72, 73 | sylan 580 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐽) → ((◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴) ↔ ((◡𝐹 “ 𝑥) ∈ 𝐽 ∧ (◡𝐹 “ 𝑥) ⊆ 𝐴))) | 
| 75 | 74 | simprbda 498 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ 𝐽) ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴)) → (◡𝐹 “ 𝑥) ∈ 𝐽) | 
| 76 | 75 | adantrl 716 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ 𝐽) ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) → (◡𝐹 “ 𝑥) ∈ 𝐽) | 
| 77 | 76 | an32s 652 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ 𝐽) → (◡𝐹 “ 𝑥) ∈ 𝐽) | 
| 78 |  | elqtop3 23712 | . . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽))) | 
| 79 | 1, 2, 78 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽))) | 
| 80 | 79 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ 𝐽) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽))) | 
| 81 | 70, 77, 80 | mpbir2and 713 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ 𝐽) → 𝑥 ∈ (𝐽 qTop 𝐹)) | 
| 82 |  | elrestr 17474 | . . . . . . . . . 10
⊢ (((𝐽 qTop 𝐹) ∈ Top ∧ 𝑈 ∈ V ∧ 𝑥 ∈ (𝐽 qTop 𝐹)) → (𝑥 ∩ 𝑈) ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)) | 
| 83 | 62, 68, 81, 82 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ 𝐽) → (𝑥 ∩ 𝑈) ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)) | 
| 84 | 59, 83 | eqeltrrd 2841 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ 𝐽) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)) | 
| 85 | 33 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈)) | 
| 86 |  | toponuni 22921 | . . . . . . . . . . . 12
⊢ (((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈) → 𝑈 = ∪ ((𝐽 qTop 𝐹) ↾t 𝑈)) | 
| 87 | 85, 86 | syl 17 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑈 = ∪ ((𝐽 qTop 𝐹) ↾t 𝑈)) | 
| 88 | 87 | difeq1d 4124 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈 ∖ 𝑥) = (∪ ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥)) | 
| 89 | 22 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑈 ⊆ 𝑌) | 
| 90 | 19 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) | 
| 91 |  | toponuni 22921 | . . . . . . . . . . . . 13
⊢ ((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹)) | 
| 92 | 90, 91 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑌 = ∪ (𝐽 qTop 𝐹)) | 
| 93 | 89, 92 | sseqtrd 4019 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑈 ⊆ ∪ (𝐽 qTop 𝐹)) | 
| 94 | 89 | ssdifssd 4146 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈 ∖ 𝑥) ⊆ 𝑌) | 
| 95 | 39 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → Fun 𝐹) | 
| 96 |  | funcnvcnv 6632 | . . . . . . . . . . . . . . 15
⊢ (Fun
𝐹 → Fun ◡◡𝐹) | 
| 97 |  | imadif 6649 | . . . . . . . . . . . . . . 15
⊢ (Fun
◡◡𝐹 → (◡𝐹 “ (𝑈 ∖ 𝑥)) = ((◡𝐹 “ 𝑈) ∖ (◡𝐹 “ 𝑥))) | 
| 98 | 95, 96, 97 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (◡𝐹 “ (𝑈 ∖ 𝑥)) = ((◡𝐹 “ 𝑈) ∖ (◡𝐹 “ 𝑥))) | 
| 99 | 7 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝐴 = (◡𝐹 “ 𝑈)) | 
| 100 | 99 | difeq1d 4124 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (◡𝐹 “ 𝑥)) = ((◡𝐹 “ 𝑈) ∖ (◡𝐹 “ 𝑥))) | 
| 101 | 98, 100 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (◡𝐹 “ (𝑈 ∖ 𝑥)) = (𝐴 ∖ (◡𝐹 “ 𝑥))) | 
| 102 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝐴 ∈ (Clsd‘𝐽)) | 
| 103 | 37 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴)) | 
| 104 |  | toponuni 22921 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) | 
| 105 | 103, 104 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) | 
| 106 | 105 | difeq1d 4124 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (◡𝐹 “ 𝑥)) = (∪ (𝐽 ↾t 𝐴) ∖ (◡𝐹 “ 𝑥))) | 
| 107 |  | topontop 22920 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴) → (𝐽 ↾t 𝐴) ∈ Top) | 
| 108 | 103, 107 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝐴) ∈ Top) | 
| 109 |  | simplrr 777 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴)) | 
| 110 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢ ∪ (𝐽
↾t 𝐴) =
∪ (𝐽 ↾t 𝐴) | 
| 111 | 110 | opncld 23042 | . . . . . . . . . . . . . . . 16
⊢ (((𝐽 ↾t 𝐴) ∈ Top ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴)) → (∪
(𝐽 ↾t
𝐴) ∖ (◡𝐹 “ 𝑥)) ∈ (Clsd‘(𝐽 ↾t 𝐴))) | 
| 112 | 108, 109,
111 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (∪
(𝐽 ↾t
𝐴) ∖ (◡𝐹 “ 𝑥)) ∈ (Clsd‘(𝐽 ↾t 𝐴))) | 
| 113 | 106, 112 | eqeltrd 2840 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (◡𝐹 “ 𝑥)) ∈ (Clsd‘(𝐽 ↾t 𝐴))) | 
| 114 |  | restcldr 23183 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (Clsd‘𝐽) ∧ (𝐴 ∖ (◡𝐹 “ 𝑥)) ∈ (Clsd‘(𝐽 ↾t 𝐴))) → (𝐴 ∖ (◡𝐹 “ 𝑥)) ∈ (Clsd‘𝐽)) | 
| 115 | 102, 113,
114 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (◡𝐹 “ 𝑥)) ∈ (Clsd‘𝐽)) | 
| 116 | 101, 115 | eqeltrd 2840 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (◡𝐹 “ (𝑈 ∖ 𝑥)) ∈ (Clsd‘𝐽)) | 
| 117 |  | qtopcld 23722 | . . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → ((𝑈 ∖ 𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ ((𝑈 ∖ 𝑥) ⊆ 𝑌 ∧ (◡𝐹 “ (𝑈 ∖ 𝑥)) ∈ (Clsd‘𝐽)))) | 
| 118 | 1, 2, 117 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 ∖ 𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ ((𝑈 ∖ 𝑥) ⊆ 𝑌 ∧ (◡𝐹 “ (𝑈 ∖ 𝑥)) ∈ (Clsd‘𝐽)))) | 
| 119 | 118 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝑈 ∖ 𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ ((𝑈 ∖ 𝑥) ⊆ 𝑌 ∧ (◡𝐹 “ (𝑈 ∖ 𝑥)) ∈ (Clsd‘𝐽)))) | 
| 120 | 94, 116, 119 | mpbir2and 713 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈 ∖ 𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹))) | 
| 121 |  | difssd 4136 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈 ∖ 𝑥) ⊆ 𝑈) | 
| 122 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ ∪ (𝐽
qTop 𝐹) = ∪ (𝐽
qTop 𝐹) | 
| 123 | 122 | restcldi 23182 | . . . . . . . . . . 11
⊢ ((𝑈 ⊆ ∪ (𝐽
qTop 𝐹) ∧ (𝑈 ∖ 𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ∧ (𝑈 ∖ 𝑥) ⊆ 𝑈) → (𝑈 ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈))) | 
| 124 | 93, 120, 121, 123 | syl3anc 1372 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈 ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈))) | 
| 125 | 88, 124 | eqeltrrd 2841 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (∪
((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈))) | 
| 126 |  | topontop 22920 | . . . . . . . . . . 11
⊢ (((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ Top) | 
| 127 | 85, 126 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ Top) | 
| 128 |  | simplrl 776 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑥 ⊆ 𝑈) | 
| 129 | 128, 87 | sseqtrd 4019 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑥 ⊆ ∪ ((𝐽 qTop 𝐹) ↾t 𝑈)) | 
| 130 |  | eqid 2736 | . . . . . . . . . . 11
⊢ ∪ ((𝐽
qTop 𝐹) ↾t
𝑈) = ∪ ((𝐽
qTop 𝐹) ↾t
𝑈) | 
| 131 | 130 | isopn2 23041 | . . . . . . . . . 10
⊢ ((((𝐽 qTop 𝐹) ↾t 𝑈) ∈ Top ∧ 𝑥 ⊆ ∪ ((𝐽 qTop 𝐹) ↾t 𝑈)) → (𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈) ↔ (∪
((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈)))) | 
| 132 | 127, 129,
131 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈) ↔ (∪
((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈)))) | 
| 133 | 125, 132 | mpbird 257 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)) | 
| 134 |  | qtoprest.6 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 ∈ 𝐽 ∨ 𝐴 ∈ (Clsd‘𝐽))) | 
| 135 | 134 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) → (𝐴 ∈ 𝐽 ∨ 𝐴 ∈ (Clsd‘𝐽))) | 
| 136 | 84, 133, 135 | mpjaodan 960 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝑈 ∧ (◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴))) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)) | 
| 137 | 136 | expr 456 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑈) → ((◡𝐹 “ 𝑥) ∈ (𝐽 ↾t 𝐴) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))) | 
| 138 | 56, 137 | sylbid 240 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑈) → ((◡(𝐹 ↾ 𝐴) “ 𝑥) ∈ (𝐽 ↾t 𝐴) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))) | 
| 139 | 138 | expimpd 453 | . . . 4
⊢ (𝜑 → ((𝑥 ⊆ 𝑈 ∧ (◡(𝐹 ↾ 𝐴) “ 𝑥) ∈ (𝐽 ↾t 𝐴)) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))) | 
| 140 | 47, 139 | sylbid 240 | . . 3
⊢ (𝜑 → (𝑥 ∈ ((𝐽 ↾t 𝐴) qTop (𝐹 ↾ 𝐴)) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))) | 
| 141 | 140 | ssrdv 3988 | . 2
⊢ (𝜑 → ((𝐽 ↾t 𝐴) qTop (𝐹 ↾ 𝐴)) ⊆ ((𝐽 qTop 𝐹) ↾t 𝑈)) | 
| 142 | 35, 141 | eqssd 4000 | 1
⊢ (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) = ((𝐽 ↾t 𝐴) qTop (𝐹 ↾ 𝐴))) |