# 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 vex 𝑤 ∈ V
123 122 unisn { 𝑤 } = 𝑤
124 123 uneq2i ( 𝑠 { 𝑤 } ) = ( 𝑠𝑤 )
125 121 124 eqtri ( 𝑠 ∪ { 𝑤 } ) = ( 𝑠𝑤 )
126 120 125 sseqtrrdi ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐽 ∧ ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑢 ) ) ∧ ( ( 𝑤𝑢𝐴𝑤 ) ∧ ( 𝑗 ∈ ℕ ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ 𝑤 ) ) ) ∧ ( 𝑠 ∈ ( 𝒫 𝑢 ∩ Fin ) ∧ ( 𝐹 “ ( 1 ... 𝑗 ) ) ⊆ 𝑠 ) ) → ( ran 𝐹 ∪ { 𝐴 } ) ⊆ ( 𝑠 ∪ { 𝑤 } ) )
127 unieq ( 𝑣 = ( 𝑠 ∪ { 𝑤 } ) → 𝑣 = ( 𝑠 ∪ { 𝑤 } ) )
128 127 sseq2d ( 𝑣 = ( 𝑠 ∪ { 𝑤 } ) → ( ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑣 ↔ ( ran 𝐹 ∪ { 𝐴 } ) ⊆ ( 𝑠 ∪ { 𝑤 } ) ) )
129 128 rspcev ( ( ( 𝑠 ∪ { 𝑤 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) ∧ ( ran 𝐹 ∪ { 𝐴 } ) ⊆ ( 𝑠 ∪ { 𝑤 } ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑣 )
130 79 126 129 syl2anc ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐽 ∧ ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑢 ) ) ∧ ( ( 𝑤𝑢𝐴𝑤 ) ∧ ( 𝑗 ∈ ℕ ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ 𝑤 ) ) ) ∧ ( 𝑠 ∈ ( 𝒫 𝑢 ∩ Fin ) ∧ ( 𝐹 “ ( 1 ... 𝑗 ) ) ⊆ 𝑠 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑣 )
131 64 130 rexlimddv ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐽 ∧ ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑢 ) ) ∧ ( ( 𝑤𝑢𝐴𝑤 ) ∧ ( 𝑗 ∈ ℕ ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ 𝑤 ) ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑣 )
132 131 anassrs ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐽 ∧ ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑢 ) ) ∧ ( 𝑤𝑢𝐴𝑤 ) ) ∧ ( 𝑗 ∈ ℕ ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ 𝑤 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑣 )
133 23 132 rexlimddv ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐽 ∧ ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑢 ) ) ∧ ( 𝑤𝑢𝐴𝑤 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑣 )
134 14 133 rexlimddv ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐽 ∧ ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑢 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑣 )
135 134 expr ( ( 𝜑𝑢 ∈ 𝒫 𝐽 ) → ( ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑣 ) )
136 135 ralrimiva ( 𝜑 → ∀ 𝑢 ∈ 𝒫 𝐽 ( ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑣 ) )
137 7 snssd ( 𝜑 → { 𝐴 } ⊆ 𝑋 )
138 29 137 unssd ( 𝜑 → ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑋 )
139 138 55 sseqtrd ( 𝜑 → ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝐽 )
140 57 cmpsub ( ( 𝐽 ∈ Top ∧ ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝐽 ) → ( ( 𝐽t ( ran 𝐹 ∪ { 𝐴 } ) ) ∈ Comp ↔ ∀ 𝑢 ∈ 𝒫 𝐽 ( ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑣 ) ) )
141 53 139 140 syl2anc ( 𝜑 → ( ( 𝐽t ( ran 𝐹 ∪ { 𝐴 } ) ) ∈ Comp ↔ ∀ 𝑢 ∈ 𝒫 𝐽 ( ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( ran 𝐹 ∪ { 𝐴 } ) ⊆ 𝑣 ) ) )
142 136 141 mpbird ( 𝜑 → ( 𝐽t ( ran 𝐹 ∪ { 𝐴 } ) ) ∈ Comp )