# Metamath Proof Explorer

## Theorem 1stckgenlem

Description: The one-point compactification of NN is compact. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypotheses 1stckgen.1 $⊢ φ → J ∈ TopOn ⁡ X$
1stckgen.2 $⊢ φ → F : ℕ ⟶ X$
1stckgen.3
Assertion 1stckgenlem $⊢ φ → J ↾ 𝑡 ran ⁡ F ∪ A ∈ Comp$

### Proof

Step Hyp Ref Expression
1 1stckgen.1 $⊢ φ → J ∈ TopOn ⁡ X$
2 1stckgen.2 $⊢ φ → F : ℕ ⟶ X$
3 1stckgen.3
4 simprr $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u → ran ⁡ F ∪ A ⊆ ⋃ u$
5 ssun2 $⊢ A ⊆ ran ⁡ F ∪ A$
6 lmcl
7 1 3 6 syl2anc $⊢ φ → A ∈ X$
8 snssg $⊢ A ∈ X → A ∈ ran ⁡ F ∪ A ↔ A ⊆ ran ⁡ F ∪ A$
9 7 8 syl $⊢ φ → A ∈ ran ⁡ F ∪ A ↔ A ⊆ ran ⁡ F ∪ A$
10 5 9 mpbiri $⊢ φ → A ∈ ran ⁡ F ∪ A$
11 10 adantr $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u → A ∈ ran ⁡ F ∪ A$
12 4 11 sseldd $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u → A ∈ ⋃ u$
13 eluni2 $⊢ A ∈ ⋃ u ↔ ∃ w ∈ u A ∈ w$
14 12 13 sylib $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u → ∃ w ∈ u A ∈ w$
15 nnuz $⊢ ℕ = ℤ ≥ 1$
16 simprr $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w → A ∈ w$
17 1zzd $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w → 1 ∈ ℤ$
19 simplrl $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w → u ∈ 𝒫 J$
20 19 elpwid $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w → u ⊆ J$
21 simprl $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w → w ∈ u$
22 20 21 sseldd $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w → w ∈ J$
23 15 16 17 18 22 lmcvg $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w → ∃ j ∈ ℕ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w$
24 imassrn $⊢ F 1 … j ⊆ ran ⁡ F$
25 ssun1 $⊢ ran ⁡ F ⊆ ran ⁡ F ∪ A$
26 24 25 sstri $⊢ F 1 … j ⊆ ran ⁡ F ∪ A$
27 id $⊢ ran ⁡ F ∪ A ⊆ ⋃ u → ran ⁡ F ∪ A ⊆ ⋃ u$
28 26 27 sstrid $⊢ ran ⁡ F ∪ A ⊆ ⋃ u → F 1 … j ⊆ ⋃ u$
29 2 frnd $⊢ φ → ran ⁡ F ⊆ X$
30 24 29 sstrid $⊢ φ → F 1 … j ⊆ X$
31 resttopon $⊢ J ∈ TopOn ⁡ X ∧ F 1 … j ⊆ X → J ↾ 𝑡 F 1 … j ∈ TopOn ⁡ F 1 … j$
32 1 30 31 syl2anc $⊢ φ → J ↾ 𝑡 F 1 … j ∈ TopOn ⁡ F 1 … j$
33 topontop $⊢ J ↾ 𝑡 F 1 … j ∈ TopOn ⁡ F 1 … j → J ↾ 𝑡 F 1 … j ∈ Top$
34 32 33 syl $⊢ φ → J ↾ 𝑡 F 1 … j ∈ Top$
35 fzfid $⊢ φ → 1 … j ∈ Fin$
36 2 ffund $⊢ φ → Fun ⁡ F$
37 fz1ssnn $⊢ 1 … j ⊆ ℕ$
38 2 fdmd $⊢ φ → dom ⁡ F = ℕ$
39 37 38 sseqtrrid $⊢ φ → 1 … j ⊆ dom ⁡ F$
40 fores $⊢ Fun ⁡ F ∧ 1 … j ⊆ dom ⁡ F → F ↾ 1 … j : 1 … j ⟶ onto F 1 … j$
41 36 39 40 syl2anc $⊢ φ → F ↾ 1 … j : 1 … j ⟶ onto F 1 … j$
42 fofi $⊢ 1 … j ∈ Fin ∧ F ↾ 1 … j : 1 … j ⟶ onto F 1 … j → F 1 … j ∈ Fin$
43 35 41 42 syl2anc $⊢ φ → F 1 … j ∈ Fin$
44 pwfi $⊢ F 1 … j ∈ Fin ↔ 𝒫 F 1 … j ∈ Fin$
45 43 44 sylib $⊢ φ → 𝒫 F 1 … j ∈ Fin$
46 restsspw $⊢ J ↾ 𝑡 F 1 … j ⊆ 𝒫 F 1 … j$
47 ssfi $⊢ 𝒫 F 1 … j ∈ Fin ∧ J ↾ 𝑡 F 1 … j ⊆ 𝒫 F 1 … j → J ↾ 𝑡 F 1 … j ∈ Fin$
48 45 46 47 sylancl $⊢ φ → J ↾ 𝑡 F 1 … j ∈ Fin$
49 34 48 elind $⊢ φ → J ↾ 𝑡 F 1 … j ∈ Top ∩ Fin$
50 fincmp $⊢ J ↾ 𝑡 F 1 … j ∈ Top ∩ Fin → J ↾ 𝑡 F 1 … j ∈ Comp$
51 49 50 syl $⊢ φ → J ↾ 𝑡 F 1 … j ∈ Comp$
52 topontop $⊢ J ∈ TopOn ⁡ X → J ∈ Top$
53 1 52 syl $⊢ φ → J ∈ Top$
54 toponuni $⊢ J ∈ TopOn ⁡ X → X = ⋃ J$
55 1 54 syl $⊢ φ → X = ⋃ J$
56 30 55 sseqtrd $⊢ φ → F 1 … j ⊆ ⋃ J$
57 eqid $⊢ ⋃ J = ⋃ J$
58 57 cmpsub $⊢ J ∈ Top ∧ F 1 … j ⊆ ⋃ J → J ↾ 𝑡 F 1 … j ∈ Comp ↔ ∀ u ∈ 𝒫 J F 1 … j ⊆ ⋃ u → ∃ s ∈ 𝒫 u ∩ Fin F 1 … j ⊆ ⋃ s$
59 53 56 58 syl2anc $⊢ φ → J ↾ 𝑡 F 1 … j ∈ Comp ↔ ∀ u ∈ 𝒫 J F 1 … j ⊆ ⋃ u → ∃ s ∈ 𝒫 u ∩ Fin F 1 … j ⊆ ⋃ s$
60 51 59 mpbid $⊢ φ → ∀ u ∈ 𝒫 J F 1 … j ⊆ ⋃ u → ∃ s ∈ 𝒫 u ∩ Fin F 1 … j ⊆ ⋃ s$
61 60 r19.21bi $⊢ φ ∧ u ∈ 𝒫 J → F 1 … j ⊆ ⋃ u → ∃ s ∈ 𝒫 u ∩ Fin F 1 … j ⊆ ⋃ s$
62 28 61 syl5 $⊢ φ ∧ u ∈ 𝒫 J → ran ⁡ F ∪ A ⊆ ⋃ u → ∃ s ∈ 𝒫 u ∩ Fin F 1 … j ⊆ ⋃ s$
63 62 impr $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u → ∃ s ∈ 𝒫 u ∩ Fin F 1 … j ⊆ ⋃ s$
64 63 adantr $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w → ∃ s ∈ 𝒫 u ∩ Fin F 1 … j ⊆ ⋃ s$
65 simprl $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → s ∈ 𝒫 u ∩ Fin$
66 65 elin1d $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → s ∈ 𝒫 u$
67 66 elpwid $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → s ⊆ u$
68 simprll $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w → w ∈ u$
69 68 adantr $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → w ∈ u$
70 69 snssd $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → w ⊆ u$
71 67 70 unssd $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → s ∪ w ⊆ u$
72 vex $⊢ u ∈ V$
73 72 elpw2 $⊢ s ∪ w ∈ 𝒫 u ↔ s ∪ w ⊆ u$
74 71 73 sylibr $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → s ∪ w ∈ 𝒫 u$
75 65 elin2d $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → s ∈ Fin$
76 snfi $⊢ w ∈ Fin$
77 unfi $⊢ s ∈ Fin ∧ w ∈ Fin → s ∪ w ∈ Fin$
78 75 76 77 sylancl $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → s ∪ w ∈ Fin$
79 74 78 elind $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → s ∪ w ∈ 𝒫 u ∩ Fin$
80 2 ffnd $⊢ φ → F Fn ℕ$
81 80 ad3antrrr $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → F Fn ℕ$
82 simprrr $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w → ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w$
83 82 adantr $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w$
84 fveq2 $⊢ k = n → F ⁡ k = F ⁡ n$
85 84 eleq1d $⊢ k = n → F ⁡ k ∈ w ↔ F ⁡ n ∈ w$
86 85 rspccva $⊢ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ n ∈ ℤ ≥ j → F ⁡ n ∈ w$
87 83 86 sylan $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s ∧ n ∈ ℤ ≥ j → F ⁡ n ∈ w$
88 elun2 $⊢ F ⁡ n ∈ w → F ⁡ n ∈ ⋃ s ∪ w$
89 87 88 syl $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s ∧ n ∈ ℤ ≥ j → F ⁡ n ∈ ⋃ s ∪ w$
90 89 adantlr $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s ∧ n ∈ ℕ ∧ n ∈ ℤ ≥ j → F ⁡ n ∈ ⋃ s ∪ w$
91 elnnuz $⊢ n ∈ ℕ ↔ n ∈ ℤ ≥ 1$
92 91 anbi1i $⊢ n ∈ ℕ ∧ j ∈ ℤ ≥ n ↔ n ∈ ℤ ≥ 1 ∧ j ∈ ℤ ≥ n$
93 elfzuzb $⊢ n ∈ 1 … j ↔ n ∈ ℤ ≥ 1 ∧ j ∈ ℤ ≥ n$
94 92 93 bitr4i $⊢ n ∈ ℕ ∧ j ∈ ℤ ≥ n ↔ n ∈ 1 … j$
95 simprr $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → F 1 … j ⊆ ⋃ s$
96 funimass4 $⊢ Fun ⁡ F ∧ 1 … j ⊆ dom ⁡ F → F 1 … j ⊆ ⋃ s ↔ ∀ n ∈ 1 … j F ⁡ n ∈ ⋃ s$
97 36 39 96 syl2anc $⊢ φ → F 1 … j ⊆ ⋃ s ↔ ∀ n ∈ 1 … j F ⁡ n ∈ ⋃ s$
98 97 ad3antrrr $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → F 1 … j ⊆ ⋃ s ↔ ∀ n ∈ 1 … j F ⁡ n ∈ ⋃ s$
99 95 98 mpbid $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → ∀ n ∈ 1 … j F ⁡ n ∈ ⋃ s$
100 99 r19.21bi $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s ∧ n ∈ 1 … j → F ⁡ n ∈ ⋃ s$
101 elun1 $⊢ F ⁡ n ∈ ⋃ s → F ⁡ n ∈ ⋃ s ∪ w$
102 100 101 syl $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s ∧ n ∈ 1 … j → F ⁡ n ∈ ⋃ s ∪ w$
103 94 102 sylan2b $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s ∧ n ∈ ℕ ∧ j ∈ ℤ ≥ n → F ⁡ n ∈ ⋃ s ∪ w$
104 103 anassrs $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s ∧ n ∈ ℕ ∧ j ∈ ℤ ≥ n → F ⁡ n ∈ ⋃ s ∪ w$
105 simprl $⊢ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w → j ∈ ℕ$
106 105 ad2antlr $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → j ∈ ℕ$
107 nnz $⊢ j ∈ ℕ → j ∈ ℤ$
108 nnz $⊢ n ∈ ℕ → n ∈ ℤ$
109 uztric $⊢ j ∈ ℤ ∧ n ∈ ℤ → n ∈ ℤ ≥ j ∨ j ∈ ℤ ≥ n$
110 107 108 109 syl2an $⊢ j ∈ ℕ ∧ n ∈ ℕ → n ∈ ℤ ≥ j ∨ j ∈ ℤ ≥ n$
111 106 110 sylan $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s ∧ n ∈ ℕ → n ∈ ℤ ≥ j ∨ j ∈ ℤ ≥ n$
112 90 104 111 mpjaodan $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s ∧ n ∈ ℕ → F ⁡ n ∈ ⋃ s ∪ w$
113 112 ralrimiva $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → ∀ n ∈ ℕ F ⁡ n ∈ ⋃ s ∪ w$
114 fnfvrnss $⊢ F Fn ℕ ∧ ∀ n ∈ ℕ F ⁡ n ∈ ⋃ s ∪ w → ran ⁡ F ⊆ ⋃ s ∪ w$
115 81 113 114 syl2anc $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → ran ⁡ F ⊆ ⋃ s ∪ w$
116 elun2 $⊢ A ∈ w → A ∈ ⋃ s ∪ w$
117 116 ad2antlr $⊢ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w → A ∈ ⋃ s ∪ w$
118 117 ad2antlr $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → A ∈ ⋃ s ∪ w$
119 118 snssd $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → A ⊆ ⋃ s ∪ w$
120 115 119 unssd $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → ran ⁡ F ∪ A ⊆ ⋃ s ∪ w$
121 uniun $⊢ ⋃ s ∪ w = ⋃ s ∪ ⋃ w$
122 vex $⊢ w ∈ V$
123 122 unisn $⊢ ⋃ w = w$
124 123 uneq2i $⊢ ⋃ s ∪ ⋃ w = ⋃ s ∪ w$
125 121 124 eqtri $⊢ ⋃ s ∪ w = ⋃ s ∪ w$
126 120 125 sseqtrrdi $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → ran ⁡ F ∪ A ⊆ ⋃ s ∪ w$
127 unieq $⊢ v = s ∪ w → ⋃ v = ⋃ s ∪ w$
128 127 sseq2d $⊢ v = s ∪ w → ran ⁡ F ∪ A ⊆ ⋃ v ↔ ran ⁡ F ∪ A ⊆ ⋃ s ∪ w$
129 128 rspcev $⊢ s ∪ w ∈ 𝒫 u ∩ Fin ∧ ran ⁡ F ∪ A ⊆ ⋃ s ∪ w → ∃ v ∈ 𝒫 u ∩ Fin ran ⁡ F ∪ A ⊆ ⋃ v$
130 79 126 129 syl2anc $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w ∧ s ∈ 𝒫 u ∩ Fin ∧ F 1 … j ⊆ ⋃ s → ∃ v ∈ 𝒫 u ∩ Fin ran ⁡ F ∪ A ⊆ ⋃ v$
131 64 130 rexlimddv $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w → ∃ v ∈ 𝒫 u ∩ Fin ran ⁡ F ∪ A ⊆ ⋃ v$
132 131 anassrs $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k ∈ w → ∃ v ∈ 𝒫 u ∩ Fin ran ⁡ F ∪ A ⊆ ⋃ v$
133 23 132 rexlimddv $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u ∧ w ∈ u ∧ A ∈ w → ∃ v ∈ 𝒫 u ∩ Fin ran ⁡ F ∪ A ⊆ ⋃ v$
134 14 133 rexlimddv $⊢ φ ∧ u ∈ 𝒫 J ∧ ran ⁡ F ∪ A ⊆ ⋃ u → ∃ v ∈ 𝒫 u ∩ Fin ran ⁡ F ∪ A ⊆ ⋃ v$
135 134 expr $⊢ φ ∧ u ∈ 𝒫 J → ran ⁡ F ∪ A ⊆ ⋃ u → ∃ v ∈ 𝒫 u ∩ Fin ran ⁡ F ∪ A ⊆ ⋃ v$
136 135 ralrimiva $⊢ φ → ∀ u ∈ 𝒫 J ran ⁡ F ∪ A ⊆ ⋃ u → ∃ v ∈ 𝒫 u ∩ Fin ran ⁡ F ∪ A ⊆ ⋃ v$
137 7 snssd $⊢ φ → A ⊆ X$
138 29 137 unssd $⊢ φ → ran ⁡ F ∪ A ⊆ X$
139 138 55 sseqtrd $⊢ φ → ran ⁡ F ∪ A ⊆ ⋃ J$
140 57 cmpsub $⊢ J ∈ Top ∧ ran ⁡ F ∪ A ⊆ ⋃ J → J ↾ 𝑡 ran ⁡ F ∪ A ∈ Comp ↔ ∀ u ∈ 𝒫 J ran ⁡ F ∪ A ⊆ ⋃ u → ∃ v ∈ 𝒫 u ∩ Fin ran ⁡ F ∪ A ⊆ ⋃ v$
141 53 139 140 syl2anc $⊢ φ → J ↾ 𝑡 ran ⁡ F ∪ A ∈ Comp ↔ ∀ u ∈ 𝒫 J ran ⁡ F ∪ A ⊆ ⋃ u → ∃ v ∈ 𝒫 u ∩ Fin ran ⁡ F ∪ A ⊆ ⋃ v$
142 136 141 mpbird $⊢ φ → J ↾ 𝑡 ran ⁡ F ∪ A ∈ Comp$