| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | locfinref.4 | . . . 4
⊢ (𝜑 → 𝑉Ref𝑈) | 
| 2 |  | locfinref.5 | . . . . 5
⊢ (𝜑 → 𝑉 ∈ (LocFin‘𝐽)) | 
| 3 |  | reff 33839 | . . . . 5
⊢ (𝑉 ∈ (LocFin‘𝐽) → (𝑉Ref𝑈 ↔ (∪ 𝑈 ⊆ ∪ 𝑉
∧ ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))))) | 
| 4 | 2, 3 | syl 17 | . . . 4
⊢ (𝜑 → (𝑉Ref𝑈 ↔ (∪ 𝑈 ⊆ ∪ 𝑉
∧ ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))))) | 
| 5 | 1, 4 | mpbid 232 | . . 3
⊢ (𝜑 → (∪ 𝑈
⊆ ∪ 𝑉 ∧ ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)))) | 
| 6 | 5 | simprd 495 | . 2
⊢ (𝜑 → ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))) | 
| 7 |  | funmpt 6603 | . . . . . 6
⊢ Fun
(𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) | 
| 8 | 7 | a1i 11 | . . . . 5
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) | 
| 9 |  | eqid 2736 | . . . . . . 7
⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) | 
| 10 | 9 | dmmptss 6260 | . . . . . 6
⊢ dom
(𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ ran 𝑔 | 
| 11 |  | frn 6742 | . . . . . . 7
⊢ (𝑔:𝑉⟶𝑈 → ran 𝑔 ⊆ 𝑈) | 
| 12 | 11 | ad2antlr 727 | . . . . . 6
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran 𝑔 ⊆ 𝑈) | 
| 13 | 10, 12 | sstrid 3994 | . . . . 5
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈) | 
| 14 |  | locfintop 23530 | . . . . . . . . . 10
⊢ (𝑉 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top) | 
| 15 | 2, 14 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ Top) | 
| 16 | 15 | ad3antrrr 730 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝐽 ∈ Top) | 
| 17 |  | cnvimass 6099 | . . . . . . . . . 10
⊢ (◡𝑔 “ {𝑢}) ⊆ dom 𝑔 | 
| 18 |  | fdm 6744 | . . . . . . . . . . 11
⊢ (𝑔:𝑉⟶𝑈 → dom 𝑔 = 𝑉) | 
| 19 | 18 | ad3antlr 731 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → dom 𝑔 = 𝑉) | 
| 20 | 17, 19 | sseqtrid 4025 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (◡𝑔 “ {𝑢}) ⊆ 𝑉) | 
| 21 |  | locfinref.3 | . . . . . . . . . 10
⊢ (𝜑 → 𝑉 ⊆ 𝐽) | 
| 22 | 21 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝑉 ⊆ 𝐽) | 
| 23 | 20, 22 | sstrd 3993 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (◡𝑔 “ {𝑢}) ⊆ 𝐽) | 
| 24 |  | uniopn 22904 | . . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ (◡𝑔 “ {𝑢}) ⊆ 𝐽) → ∪ (◡𝑔 “ {𝑢}) ∈ 𝐽) | 
| 25 | 16, 23, 24 | syl2anc 584 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → ∪ (◡𝑔 “ {𝑢}) ∈ 𝐽) | 
| 26 | 25 | ralrimiva 3145 | . . . . . 6
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∀𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ∈ 𝐽) | 
| 27 | 9 | rnmptss 7142 | . . . . . 6
⊢
(∀𝑢 ∈
ran 𝑔∪ (◡𝑔 “ {𝑢}) ∈ 𝐽 → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽) | 
| 28 | 26, 27 | syl 17 | . . . . 5
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽) | 
| 29 |  | eqid 2736 | . . . . . . . . . 10
⊢ ∪ 𝑉 =
∪ 𝑉 | 
| 30 |  | eqid 2736 | . . . . . . . . . 10
⊢ ∪ 𝑈 =
∪ 𝑈 | 
| 31 | 29, 30 | refbas 23519 | . . . . . . . . 9
⊢ (𝑉Ref𝑈 → ∪ 𝑈 = ∪
𝑉) | 
| 32 | 1, 31 | syl 17 | . . . . . . . 8
⊢ (𝜑 → ∪ 𝑈 =
∪ 𝑉) | 
| 33 | 32 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑈 = ∪
𝑉) | 
| 34 |  | nfv 1913 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑣(𝜑 ∧ 𝑔:𝑉⟶𝑈) | 
| 35 |  | nfra1 3283 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑣∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣) | 
| 36 | 34, 35 | nfan 1898 | . . . . . . . . . . . 12
⊢
Ⅎ𝑣((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) | 
| 37 |  | nfre1 3284 | . . . . . . . . . . . 12
⊢
Ⅎ𝑣∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 | 
| 38 | 36, 37 | nfan 1898 | . . . . . . . . . . 11
⊢
Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) | 
| 39 |  | ffn 6735 | . . . . . . . . . . . . . . 15
⊢ (𝑔:𝑉⟶𝑈 → 𝑔 Fn 𝑉) | 
| 40 | 39 | ad4antlr 733 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → 𝑔 Fn 𝑉) | 
| 41 |  | simplr 768 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ 𝑉) | 
| 42 |  | fnfvelrn 7099 | . . . . . . . . . . . . . 14
⊢ ((𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉) → (𝑔‘𝑣) ∈ ran 𝑔) | 
| 43 | 40, 41, 42 | syl2anc 584 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → (𝑔‘𝑣) ∈ ran 𝑔) | 
| 44 |  | ssid 4005 | . . . . . . . . . . . . . . 15
⊢ 𝑣 ⊆ 𝑣 | 
| 45 | 39 | ad3antlr 731 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) → 𝑔 Fn 𝑉) | 
| 46 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢ (𝑔‘𝑣) = (𝑔‘𝑣) | 
| 47 |  | fniniseg 7079 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑔 Fn 𝑉 → (𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}) ↔ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = (𝑔‘𝑣)))) | 
| 48 | 47 | biimpar 477 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑔 Fn 𝑉 ∧ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = (𝑔‘𝑣))) → 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)})) | 
| 49 | 46, 48 | mpanr2 704 | . . . . . . . . . . . . . . . 16
⊢ ((𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)})) | 
| 50 | 45, 49 | sylancom 588 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)})) | 
| 51 |  | ssuni 4931 | . . . . . . . . . . . . . . 15
⊢ ((𝑣 ⊆ 𝑣 ∧ 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)})) → 𝑣 ⊆ ∪ (◡𝑔 “ {(𝑔‘𝑣)})) | 
| 52 | 44, 50, 51 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) → 𝑣 ⊆ ∪ (◡𝑔 “ {(𝑔‘𝑣)})) | 
| 53 | 52 | sselda 3982 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ ∪ (◡𝑔 “ {(𝑔‘𝑣)})) | 
| 54 |  | sneq 4635 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑔‘𝑣) → {𝑢} = {(𝑔‘𝑣)}) | 
| 55 | 54 | imaeq2d 6077 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 = (𝑔‘𝑣) → (◡𝑔 “ {𝑢}) = (◡𝑔 “ {(𝑔‘𝑣)})) | 
| 56 | 55 | unieqd 4919 | . . . . . . . . . . . . . . 15
⊢ (𝑢 = (𝑔‘𝑣) → ∪ (◡𝑔 “ {𝑢}) = ∪ (◡𝑔 “ {(𝑔‘𝑣)})) | 
| 57 | 56 | eleq2d 2826 | . . . . . . . . . . . . . 14
⊢ (𝑢 = (𝑔‘𝑣) → (𝑥 ∈ ∪ (◡𝑔 “ {𝑢}) ↔ 𝑥 ∈ ∪ (◡𝑔 “ {(𝑔‘𝑣)}))) | 
| 58 | 57 | rspcev 3621 | . . . . . . . . . . . . 13
⊢ (((𝑔‘𝑣) ∈ ran 𝑔 ∧ 𝑥 ∈ ∪ (◡𝑔 “ {(𝑔‘𝑣)})) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) | 
| 59 | 43, 53, 58 | syl2anc 584 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) | 
| 60 | 59 | adantllr 719 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) | 
| 61 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) → ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) | 
| 62 | 38, 60, 61 | r19.29af 3267 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) | 
| 63 |  | nfv 1913 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑣 𝑢 ∈ ran 𝑔 | 
| 64 | 36, 63 | nfan 1898 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) | 
| 65 |  | nfv 1913 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑣 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}) | 
| 66 | 64, 65 | nfan 1898 | . . . . . . . . . . . 12
⊢
Ⅎ𝑣((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) | 
| 67 | 20 | ad3antrrr 730 | . . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → (◡𝑔 “ {𝑢}) ⊆ 𝑉) | 
| 68 |  | simplr 768 | . . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ (◡𝑔 “ {𝑢})) | 
| 69 | 67, 68 | sseldd 3983 | . . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ 𝑉) | 
| 70 |  | simpr 484 | . . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑣) | 
| 71 |  | simpr 484 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) | 
| 72 |  | eluni2 4910 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ∪ (◡𝑔 “ {𝑢}) ↔ ∃𝑣 ∈ (◡𝑔 “ {𝑢})𝑥 ∈ 𝑣) | 
| 73 | 71, 72 | sylib 218 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → ∃𝑣 ∈ (◡𝑔 “ {𝑢})𝑥 ∈ 𝑣) | 
| 74 | 66, 69, 70, 73 | reximd2a 3268 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) | 
| 75 | 74 | r19.29an 3157 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) | 
| 76 | 62, 75 | impbida 800 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 ↔ ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))) | 
| 77 |  | eluni2 4910 | . . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑉
↔ ∃𝑣 ∈
𝑉 𝑥 ∈ 𝑣) | 
| 78 |  | eliun 4994 | . . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ↔ ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) | 
| 79 | 76, 77, 78 | 3bitr4g 314 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (𝑥 ∈ ∪ 𝑉 ↔ 𝑥 ∈ ∪
𝑢 ∈ ran 𝑔∪
(◡𝑔 “ {𝑢}))) | 
| 80 | 79 | eqrdv 2734 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑉 = ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢})) | 
| 81 |  | dfiun3g 5977 | . . . . . . . 8
⊢
(∀𝑢 ∈
ran 𝑔∪ (◡𝑔 “ {𝑢}) ∈ 𝐽 → ∪
𝑢 ∈ ran 𝑔∪
(◡𝑔 “ {𝑢}) = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) | 
| 82 | 26, 81 | syl 17 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪
𝑢 ∈ ran 𝑔∪
(◡𝑔 “ {𝑢}) = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) | 
| 83 | 33, 80, 82 | 3eqtrd 2780 | . . . . . 6
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑈 = ∪
ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) | 
| 84 | 11 | ad3antlr 731 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ran 𝑔 ⊆ 𝑈) | 
| 85 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑤 ∈ V | 
| 86 | 9 | elrnmpt 5968 | . . . . . . . . . . 11
⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢}))) | 
| 87 | 85, 86 | mp1i 13 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢}))) | 
| 88 | 87 | biimpa 476 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢})) | 
| 89 |  | ssrexv 4052 | . . . . . . . . 9
⊢ (ran
𝑔 ⊆ 𝑈 → (∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢}) → ∃𝑢 ∈ 𝑈 𝑤 = ∪ (◡𝑔 “ {𝑢}))) | 
| 90 | 84, 88, 89 | sylc 65 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ∃𝑢 ∈ 𝑈 𝑤 = ∪ (◡𝑔 “ {𝑢})) | 
| 91 |  | nfv 1913 | . . . . . . . . . 10
⊢
Ⅎ𝑢((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) | 
| 92 |  | nfmpt1 5249 | . . . . . . . . . . . 12
⊢
Ⅎ𝑢(𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) | 
| 93 | 92 | nfrn 5962 | . . . . . . . . . . 11
⊢
Ⅎ𝑢ran
(𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) | 
| 94 | 93 | nfcri 2896 | . . . . . . . . . 10
⊢
Ⅎ𝑢 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) | 
| 95 | 91, 94 | nfan 1898 | . . . . . . . . 9
⊢
Ⅎ𝑢(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) | 
| 96 |  | simpr 484 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → 𝑤 = ∪ (◡𝑔 “ {𝑢})) | 
| 97 |  | nfv 1913 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑣 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) | 
| 98 | 36, 97 | nfan 1898 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) | 
| 99 |  | nfv 1913 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑣 𝑢 ∈ 𝑈 | 
| 100 | 98, 99 | nfan 1898 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑣((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) | 
| 101 |  | nfv 1913 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑣 𝑤 = ∪
(◡𝑔 “ {𝑢}) | 
| 102 | 100, 101 | nfan 1898 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑣(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) | 
| 103 |  | simp-5r 785 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) | 
| 104 | 39 | ad5antlr 735 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → 𝑔 Fn 𝑉) | 
| 105 |  | fniniseg 7079 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 Fn 𝑉 → (𝑣 ∈ (◡𝑔 “ {𝑢}) ↔ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = 𝑢))) | 
| 106 | 104, 105 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → (𝑣 ∈ (◡𝑔 “ {𝑢}) ↔ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = 𝑢))) | 
| 107 | 106 | biimpa 476 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = 𝑢)) | 
| 108 | 107 | simpld 494 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → 𝑣 ∈ 𝑉) | 
| 109 |  | rspa 3247 | . . . . . . . . . . . . . . . 16
⊢
((∀𝑣 ∈
𝑉 𝑣 ⊆ (𝑔‘𝑣) ∧ 𝑣 ∈ 𝑉) → 𝑣 ⊆ (𝑔‘𝑣)) | 
| 110 | 103, 108,
109 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → 𝑣 ⊆ (𝑔‘𝑣)) | 
| 111 | 107 | simprd 495 | . . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → (𝑔‘𝑣) = 𝑢) | 
| 112 | 110, 111 | sseqtrd 4019 | . . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → 𝑣 ⊆ 𝑢) | 
| 113 | 112 | ex 412 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → (𝑣 ∈ (◡𝑔 “ {𝑢}) → 𝑣 ⊆ 𝑢)) | 
| 114 | 102, 113 | ralrimi 3256 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → ∀𝑣 ∈ (◡𝑔 “ {𝑢})𝑣 ⊆ 𝑢) | 
| 115 |  | unissb 4938 | . . . . . . . . . . . 12
⊢ (∪ (◡𝑔 “ {𝑢}) ⊆ 𝑢 ↔ ∀𝑣 ∈ (◡𝑔 “ {𝑢})𝑣 ⊆ 𝑢) | 
| 116 | 114, 115 | sylibr 234 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → ∪
(◡𝑔 “ {𝑢}) ⊆ 𝑢) | 
| 117 | 96, 116 | eqsstrd 4017 | . . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → 𝑤 ⊆ 𝑢) | 
| 118 | 117 | exp31 419 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → (𝑢 ∈ 𝑈 → (𝑤 = ∪ (◡𝑔 “ {𝑢}) → 𝑤 ⊆ 𝑢))) | 
| 119 | 95, 118 | reximdai 3260 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → (∃𝑢 ∈ 𝑈 𝑤 = ∪ (◡𝑔 “ {𝑢}) → ∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢)) | 
| 120 | 90, 119 | mpd 15 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢) | 
| 121 | 120 | ralrimiva 3145 | . . . . . 6
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢) | 
| 122 |  | vex 3483 | . . . . . . . . . 10
⊢ 𝑔 ∈ V | 
| 123 | 122 | rnex 7933 | . . . . . . . . 9
⊢ ran 𝑔 ∈ V | 
| 124 | 123 | mptex 7244 | . . . . . . . 8
⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V | 
| 125 |  | rnexg 7925 | . . . . . . . 8
⊢ ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V) | 
| 126 | 124, 125 | mp1i 13 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V) | 
| 127 |  | eqid 2736 | . . . . . . . 8
⊢ ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) | 
| 128 | 127, 30 | isref 23518 | . . . . . . 7
⊢ (ran
(𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V → (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈 ↔ (∪ 𝑈 = ∪
ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢))) | 
| 129 | 126, 128 | syl 17 | . . . . . 6
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈 ↔ (∪ 𝑈 = ∪
ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢))) | 
| 130 | 83, 121, 129 | mpbir2and 713 | . . . . 5
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈) | 
| 131 | 15 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → 𝐽 ∈ Top) | 
| 132 |  | locfinref.2 | . . . . . . . 8
⊢ (𝜑 → 𝑋 = ∪ 𝑈) | 
| 133 | 132 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → 𝑋 = ∪ 𝑈) | 
| 134 | 133, 83 | eqtrd 2776 | . . . . . 6
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → 𝑋 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) | 
| 135 |  | nfv 1913 | . . . . . . . . 9
⊢
Ⅎ𝑣 𝑥 ∈ 𝑋 | 
| 136 | 36, 135 | nfan 1898 | . . . . . . . 8
⊢
Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) | 
| 137 |  | simplr 768 | . . . . . . . 8
⊢
((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)) → 𝑣 ∈ 𝐽) | 
| 138 |  | ffun 6738 | . . . . . . . . . . . . . 14
⊢ (𝑔:𝑉⟶𝑈 → Fun 𝑔) | 
| 139 | 138 | ad6antlr 737 | . . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → Fun 𝑔) | 
| 140 |  | imafi 9354 | . . . . . . . . . . . . 13
⊢ ((Fun
𝑔 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) ∈ Fin) | 
| 141 | 139, 140 | sylancom 588 | . . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) ∈ Fin) | 
| 142 |  | simp3 1138 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) | 
| 143 |  | sneq 4635 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝑘 → {𝑢} = {𝑘}) | 
| 144 | 143 | imaeq2d 6077 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑘 → (◡𝑔 “ {𝑢}) = (◡𝑔 “ {𝑘})) | 
| 145 | 144 | unieqd 4919 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = 𝑘 → ∪ (◡𝑔 “ {𝑢}) = ∪ (◡𝑔 “ {𝑘})) | 
| 146 | 122 | cnvex 7948 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ◡𝑔 ∈ V | 
| 147 |  | imaexg 7936 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (◡𝑔 ∈ V → (◡𝑔 “ {𝑘}) ∈ V) | 
| 148 | 146, 147 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (◡𝑔 “ {𝑘}) ∈ V | 
| 149 | 148 | uniex 7762 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ∪ (◡𝑔 “ {𝑘}) ∈ V | 
| 150 | 145, 9, 149 | fvmpt 7015 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ran 𝑔 → ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘) = ∪ (◡𝑔 “ {𝑘})) | 
| 151 | 150 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘) = ∪ (◡𝑔 “ {𝑘})) | 
| 152 | 142, 151 | eqtrd 2776 | . . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = ∪ (◡𝑔 “ {𝑘})) | 
| 153 | 152 | ineq1d 4218 | . . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → (𝑤 ∩ 𝑣) = (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣)) | 
| 154 | 153 | neeq1d 2999 | . . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → ((𝑤 ∩ 𝑣) ≠ ∅ ↔ (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅)) | 
| 155 | 123 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → ran 𝑔 ∈ V) | 
| 156 |  | imaexg 7936 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (◡𝑔 ∈ V → (◡𝑔 “ {𝑢}) ∈ V) | 
| 157 | 146, 156 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . 20
⊢ (◡𝑔 “ {𝑢}) ∈ V | 
| 158 | 157 | uniex 7762 | . . . . . . . . . . . . . . . . . . 19
⊢ ∪ (◡𝑔 “ {𝑢}) ∈ V | 
| 159 | 158, 9 | fnmpti 6710 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) Fn ran 𝑔 | 
| 160 |  | dffn4 6825 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) Fn ran 𝑔 ↔ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})):ran 𝑔–onto→ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) | 
| 161 | 159, 160 | mpbi 230 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})):ran 𝑔–onto→ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) | 
| 162 | 161 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})):ran 𝑔–onto→ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) | 
| 163 | 154, 155,
162 | rabfodom 32525 | . . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑘 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅}) | 
| 164 |  | sneq 4635 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑢 → {𝑘} = {𝑢}) | 
| 165 | 164 | imaeq2d 6077 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑢 → (◡𝑔 “ {𝑘}) = (◡𝑔 “ {𝑢})) | 
| 166 | 165 | unieqd 4919 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑢 → ∪ (◡𝑔 “ {𝑘}) = ∪ (◡𝑔 “ {𝑢})) | 
| 167 | 166 | ineq1d 4218 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑢 → (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) = (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣)) | 
| 168 | 167 | neeq1d 2999 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑢 → ((∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅ ↔ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅)) | 
| 169 | 168 | cbvrabv 3446 | . . . . . . . . . . . . . . 15
⊢ {𝑘 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅} = {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} | 
| 170 | 163, 169 | breqtrdi 5183 | . . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅}) | 
| 171 | 123 | rabex 5338 | . . . . . . . . . . . . . . 15
⊢ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢} ∈ V | 
| 172 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑗(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) | 
| 173 |  | nfrab1 3456 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑗{𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} | 
| 174 | 173 | nfel1 2921 | . . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑗{𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin | 
| 175 | 172, 174 | nfan 1898 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑗((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) | 
| 176 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑗 𝑢 ∈ ran 𝑔 | 
| 177 | 175, 176 | nfan 1898 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) | 
| 178 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗(∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ | 
| 179 | 177, 178 | nfan 1898 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) | 
| 180 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗(𝑔‘𝑘) = 𝑢 | 
| 181 | 173, 180 | nfrexw 3312 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢 | 
| 182 | 39 | ad5antlr 735 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) → 𝑔 Fn 𝑉) | 
| 183 | 182 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝜑 ∧
𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑔 Fn 𝑉) | 
| 184 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝜑 ∧
𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑗 ∈ (◡𝑔 “ {𝑢})) | 
| 185 |  | fniniseg 7079 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 Fn 𝑉 → (𝑗 ∈ (◡𝑔 “ {𝑢}) ↔ (𝑗 ∈ 𝑉 ∧ (𝑔‘𝑗) = 𝑢))) | 
| 186 | 185 | biimpa 476 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔 Fn 𝑉 ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) → (𝑗 ∈ 𝑉 ∧ (𝑔‘𝑗) = 𝑢)) | 
| 187 | 183, 184,
186 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝜑 ∧
𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → (𝑗 ∈ 𝑉 ∧ (𝑔‘𝑗) = 𝑢)) | 
| 188 | 187 | simpld 494 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((((𝜑 ∧
𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑗 ∈ 𝑉) | 
| 189 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((((𝜑 ∧
𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → (𝑗 ∩ 𝑣) ≠ ∅) | 
| 190 |  | rabid 3457 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ↔ (𝑗 ∈ 𝑉 ∧ (𝑗 ∩ 𝑣) ≠ ∅)) | 
| 191 | 188, 189,
190 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((((((𝜑 ∧
𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) | 
| 192 | 187 | simprd 495 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((((((𝜑 ∧
𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → (𝑔‘𝑗) = 𝑢) | 
| 193 |  | fveqeq2 6914 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑗 → ((𝑔‘𝑘) = 𝑢 ↔ (𝑔‘𝑗) = 𝑢)) | 
| 194 | 193 | rspcev 3621 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∧ (𝑔‘𝑗) = 𝑢) → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢) | 
| 195 | 191, 192,
194 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((((((𝜑 ∧
𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢) | 
| 196 |  | uniinn0 32564 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ ↔ ∃𝑗 ∈ (◡𝑔 “ {𝑢})(𝑗 ∩ 𝑣) ≠ ∅) | 
| 197 | 196 | biimpi 216 | . . . . . . . . . . . . . . . . . . 19
⊢ ((∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑗 ∈ (◡𝑔 “ {𝑢})(𝑗 ∩ 𝑣) ≠ ∅) | 
| 198 | 197 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑗 ∈ (◡𝑔 “ {𝑢})(𝑗 ∩ 𝑣) ≠ ∅) | 
| 199 | 179, 181,
195, 198 | r19.29af2 3266 | . . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢) | 
| 200 | 199 | ex 412 | . . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) → ((∪
(◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢)) | 
| 201 | 200 | ss2rabdv 4075 | . . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}) | 
| 202 |  | ssdomg 9041 | . . . . . . . . . . . . . . 15
⊢ ({𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢} ∈ V → ({𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢} → {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})) | 
| 203 | 171, 201,
202 | mpsyl 68 | . . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}) | 
| 204 |  | domtr 9048 | . . . . . . . . . . . . . 14
⊢ (({𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ∧ {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}) | 
| 205 | 170, 203,
204 | syl2anc 584 | . . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}) | 
| 206 | 182 | adantr 480 | . . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → 𝑔 Fn 𝑉) | 
| 207 |  | dffn3 6747 | . . . . . . . . . . . . . . 15
⊢ (𝑔 Fn 𝑉 ↔ 𝑔:𝑉⟶ran 𝑔) | 
| 208 | 207 | biimpi 216 | . . . . . . . . . . . . . 14
⊢ (𝑔 Fn 𝑉 → 𝑔:𝑉⟶ran 𝑔) | 
| 209 |  | ssrab2 4079 | . . . . . . . . . . . . . . 15
⊢ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ⊆ 𝑉 | 
| 210 |  | fimarab 6982 | . . . . . . . . . . . . . . 15
⊢ ((𝑔:𝑉⟶ran 𝑔 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ⊆ 𝑉) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}) | 
| 211 | 209, 210 | mpan2 691 | . . . . . . . . . . . . . 14
⊢ (𝑔:𝑉⟶ran 𝑔 → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}) | 
| 212 | 206, 208,
211 | 3syl 18 | . . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}) | 
| 213 | 205, 212 | breqtrrd 5170 | . . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅})) | 
| 214 |  | domfi 9230 | . . . . . . . . . . . 12
⊢ (((𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) ∈ Fin ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅})) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin) | 
| 215 | 141, 213,
214 | syl2anc 584 | . . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin) | 
| 216 | 215 | ex 412 | . . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) → ({𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)) | 
| 217 | 216 | imdistanda 571 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) → ((𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈
Fin))) | 
| 218 | 217 | imp 406 | . . . . . . . 8
⊢
((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)) → (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)) | 
| 219 |  | simplll 774 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) → 𝜑) | 
| 220 |  | locfinref.x | . . . . . . . . . . . . 13
⊢ 𝑋 = ∪
𝐽 | 
| 221 | 220, 29 | islocfin 23526 | . . . . . . . . . . . 12
⊢ (𝑉 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈
Fin))) | 
| 222 | 2, 221 | sylib 218 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈
Fin))) | 
| 223 | 222 | simp3d 1144 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)) | 
| 224 | 223 | r19.21bi 3250 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)) | 
| 225 | 219, 224 | sylancom 588 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)) | 
| 226 | 136, 137,
218, 225 | reximd2a 3268 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)) | 
| 227 | 226 | ralrimiva 3145 | . . . . . 6
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)) | 
| 228 | 220, 127 | islocfin 23526 | . . . . . 6
⊢ (ran
(𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈
Fin))) | 
| 229 | 131, 134,
227, 228 | syl3anbrc 1343 | . . . . 5
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽)) | 
| 230 |  | funeq 6585 | . . . . . . . 8
⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (Fun 𝑓 ↔ Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))) | 
| 231 |  | dmeq 5913 | . . . . . . . . 9
⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → dom 𝑓 = dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) | 
| 232 | 231 | sseq1d 4014 | . . . . . . . 8
⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (dom 𝑓 ⊆ 𝑈 ↔ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈)) | 
| 233 |  | rneq 5946 | . . . . . . . . 9
⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → ran 𝑓 = ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) | 
| 234 | 233 | sseq1d 4014 | . . . . . . . 8
⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (ran 𝑓 ⊆ 𝐽 ↔ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽)) | 
| 235 | 230, 232,
234 | 3anbi123d 1437 | . . . . . . 7
⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → ((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ↔ (Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽))) | 
| 236 | 233 | breq1d 5152 | . . . . . . . 8
⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (ran 𝑓Ref𝑈 ↔ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈)) | 
| 237 | 233 | eleq1d 2825 | . . . . . . . 8
⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (ran 𝑓 ∈ (LocFin‘𝐽) ↔ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))) | 
| 238 | 236, 237 | anbi12d 632 | . . . . . . 7
⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → ((ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)) ↔ (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽)))) | 
| 239 | 235, 238 | anbi12d 632 | . . . . . 6
⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))) ↔ ((Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽) ∧ (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))))) | 
| 240 | 124, 239 | spcev 3605 | . . . . 5
⊢ (((Fun
(𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽) ∧ (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))) | 
| 241 | 8, 13, 28, 130, 229, 240 | syl32anc 1379 | . . . 4
⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))) | 
| 242 | 241 | expl 457 | . . 3
⊢ (𝜑 → ((𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))) | 
| 243 | 242 | exlimdv 1932 | . 2
⊢ (𝜑 → (∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))) | 
| 244 | 6, 243 | mpd 15 | 1
⊢ (𝜑 → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))) |