This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
1stckgen.2 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑋 )
1stckgen.3 ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝐴 )
Assertion 1stckgenlem ( 𝜑 → ( 𝐽 ↾t ( ran 𝐹 ∪ { 𝐴 } ) ) ∈ Comp )

Proof

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