Metamath Proof Explorer

Theorem isf34lem6

Description: Lemma for isfin3-4 . (Contributed by Stefan O'Rear, 7-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Hypothesis compss.a ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
Assertion isf34lem6 ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinIII ↔ ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑦 ∈ ω ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ suc 𝑦 ) → ∪ ran 𝑓 ∈ ran 𝑓 ) ) )

Proof

Step Hyp Ref Expression
1 compss.a ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
2 elmapi ⊢ ( 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) → 𝑓 : ω ⟶ 𝒫 𝐴 )
3 1 isf34lem7 ⊢ ( ( 𝐴 ∈ FinIII ∧ 𝑓 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ ω ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ suc 𝑦 ) ) → ∪ ran 𝑓 ∈ ran 𝑓 )
4 3 3expia ⊢ ( ( 𝐴 ∈ FinIII ∧ 𝑓 : ω ⟶ 𝒫 𝐴 ) → ( ∀ 𝑦 ∈ ω ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ suc 𝑦 ) → ∪ ran 𝑓 ∈ ran 𝑓 ) )
5 2 4 sylan2 ⊢ ( ( 𝐴 ∈ FinIII ∧ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ) → ( ∀ 𝑦 ∈ ω ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ suc 𝑦 ) → ∪ ran 𝑓 ∈ ran 𝑓 ) )
6 5 ralrimiva ⊢ ( 𝐴 ∈ FinIII → ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑦 ∈ ω ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ suc 𝑦 ) → ∪ ran 𝑓 ∈ ran 𝑓 ) )
7 elmapex ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( 𝒫 𝐴 ∈ V ∧ ω ∈ V ) )
8 7 simpld ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → 𝒫 𝐴 ∈ V )
9 pwexb ⊢ ( 𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V )
10 8 9 sylibr ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → 𝐴 ∈ V )
11 1 isf34lem2 ⊢ ( 𝐴 ∈ V → 𝐹 : 𝒫 𝐴 ⟶ 𝒫 𝐴 )
12 10 11 syl ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → 𝐹 : 𝒫 𝐴 ⟶ 𝒫 𝐴 )
13 elmapi ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → 𝑔 : ω ⟶ 𝒫 𝐴 )
14 fco ⊢ ( ( 𝐹 : 𝒫 𝐴 ⟶ 𝒫 𝐴 ∧ 𝑔 : ω ⟶ 𝒫 𝐴 ) → ( 𝐹 ∘ 𝑔 ) : ω ⟶ 𝒫 𝐴 )
15 12 13 14 syl2anc ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( 𝐹 ∘ 𝑔 ) : ω ⟶ 𝒫 𝐴 )
16 elmapg ⊢ ( ( 𝒫 𝐴 ∈ V ∧ ω ∈ V ) → ( ( 𝐹 ∘ 𝑔 ) ∈ ( 𝒫 𝐴 ↑m ω ) ↔ ( 𝐹 ∘ 𝑔 ) : ω ⟶ 𝒫 𝐴 ) )
17 7 16 syl ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( ( 𝐹 ∘ 𝑔 ) ∈ ( 𝒫 𝐴 ↑m ω ) ↔ ( 𝐹 ∘ 𝑔 ) : ω ⟶ 𝒫 𝐴 ) )
18 15 17 mpbird ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( 𝐹 ∘ 𝑔 ) ∈ ( 𝒫 𝐴 ↑m ω ) )
19 fveq1 ⊢ ( 𝑓 = ( 𝐹 ∘ 𝑔 ) → ( 𝑓 ‘ 𝑦 ) = ( ( 𝐹 ∘ 𝑔 ) ‘ 𝑦 ) )
20 fveq1 ⊢ ( 𝑓 = ( 𝐹 ∘ 𝑔 ) → ( 𝑓 ‘ suc 𝑦 ) = ( ( 𝐹 ∘ 𝑔 ) ‘ suc 𝑦 ) )
21 19 20 sseq12d ⊢ ( 𝑓 = ( 𝐹 ∘ 𝑔 ) → ( ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ suc 𝑦 ) ↔ ( ( 𝐹 ∘ 𝑔 ) ‘ 𝑦 ) ⊆ ( ( 𝐹 ∘ 𝑔 ) ‘ suc 𝑦 ) ) )
22 21 ralbidv ⊢ ( 𝑓 = ( 𝐹 ∘ 𝑔 ) → ( ∀ 𝑦 ∈ ω ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ suc 𝑦 ) ↔ ∀ 𝑦 ∈ ω ( ( 𝐹 ∘ 𝑔 ) ‘ 𝑦 ) ⊆ ( ( 𝐹 ∘ 𝑔 ) ‘ suc 𝑦 ) ) )
23 rneq ⊢ ( 𝑓 = ( 𝐹 ∘ 𝑔 ) → ran 𝑓 = ran ( 𝐹 ∘ 𝑔 ) )
24 rnco2 ⊢ ran ( 𝐹 ∘ 𝑔 ) = ( 𝐹 “ ran 𝑔 )
25 23 24 eqtrdi ⊢ ( 𝑓 = ( 𝐹 ∘ 𝑔 ) → ran 𝑓 = ( 𝐹 “ ran 𝑔 ) )
26 25 unieqd ⊢ ( 𝑓 = ( 𝐹 ∘ 𝑔 ) → ∪ ran 𝑓 = ∪ ( 𝐹 “ ran 𝑔 ) )
27 26 25 eleq12d ⊢ ( 𝑓 = ( 𝐹 ∘ 𝑔 ) → ( ∪ ran 𝑓 ∈ ran 𝑓 ↔ ∪ ( 𝐹 “ ran 𝑔 ) ∈ ( 𝐹 “ ran 𝑔 ) ) )
28 22 27 imbi12d ⊢ ( 𝑓 = ( 𝐹 ∘ 𝑔 ) → ( ( ∀ 𝑦 ∈ ω ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ suc 𝑦 ) → ∪ ran 𝑓 ∈ ran 𝑓 ) ↔ ( ∀ 𝑦 ∈ ω ( ( 𝐹 ∘ 𝑔 ) ‘ 𝑦 ) ⊆ ( ( 𝐹 ∘ 𝑔 ) ‘ suc 𝑦 ) → ∪ ( 𝐹 “ ran 𝑔 ) ∈ ( 𝐹 “ ran 𝑔 ) ) ) )
29 28 rspccv ⊢ ( ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑦 ∈ ω ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ suc 𝑦 ) → ∪ ran 𝑓 ∈ ran 𝑓 ) → ( ( 𝐹 ∘ 𝑔 ) ∈ ( 𝒫 𝐴 ↑m ω ) → ( ∀ 𝑦 ∈ ω ( ( 𝐹 ∘ 𝑔 ) ‘ 𝑦 ) ⊆ ( ( 𝐹 ∘ 𝑔 ) ‘ suc 𝑦 ) → ∪ ( 𝐹 “ ran 𝑔 ) ∈ ( 𝐹 “ ran 𝑔 ) ) ) )
30 18 29 syl5 ⊢ ( ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑦 ∈ ω ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ suc 𝑦 ) → ∪ ran 𝑓 ∈ ran 𝑓 ) → ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( ∀ 𝑦 ∈ ω ( ( 𝐹 ∘ 𝑔 ) ‘ 𝑦 ) ⊆ ( ( 𝐹 ∘ 𝑔 ) ‘ suc 𝑦 ) → ∪ ( 𝐹 “ ran 𝑔 ) ∈ ( 𝐹 “ ran 𝑔 ) ) ) )
31 sscon ⊢ ( ( 𝑔 ‘ suc 𝑦 ) ⊆ ( 𝑔 ‘ 𝑦 ) → ( 𝐴 ∖ ( 𝑔 ‘ 𝑦 ) ) ⊆ ( 𝐴 ∖ ( 𝑔 ‘ suc 𝑦 ) ) )
32 13 ffvelrnda ⊢ ( ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) ∧ 𝑦 ∈ ω ) → ( 𝑔 ‘ 𝑦 ) ∈ 𝒫 𝐴 )
33 32 elpwid ⊢ ( ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) ∧ 𝑦 ∈ ω ) → ( 𝑔 ‘ 𝑦 ) ⊆ 𝐴 )
34 1 isf34lem1 ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑔 ‘ 𝑦 ) ⊆ 𝐴 ) → ( 𝐹 ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐴 ∖ ( 𝑔 ‘ 𝑦 ) ) )
35 10 33 34 syl2an2r ⊢ ( ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) ∧ 𝑦 ∈ ω ) → ( 𝐹 ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐴 ∖ ( 𝑔 ‘ 𝑦 ) ) )
36 peano2 ⊢ ( 𝑦 ∈ ω → suc 𝑦 ∈ ω )
37 ffvelrn ⊢ ( ( 𝑔 : ω ⟶ 𝒫 𝐴 ∧ suc 𝑦 ∈ ω ) → ( 𝑔 ‘ suc 𝑦 ) ∈ 𝒫 𝐴 )
38 13 36 37 syl2an ⊢ ( ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) ∧ 𝑦 ∈ ω ) → ( 𝑔 ‘ suc 𝑦 ) ∈ 𝒫 𝐴 )
39 38 elpwid ⊢ ( ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) ∧ 𝑦 ∈ ω ) → ( 𝑔 ‘ suc 𝑦 ) ⊆ 𝐴 )
40 1 isf34lem1 ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑔 ‘ suc 𝑦 ) ⊆ 𝐴 ) → ( 𝐹 ‘ ( 𝑔 ‘ suc 𝑦 ) ) = ( 𝐴 ∖ ( 𝑔 ‘ suc 𝑦 ) ) )
41 10 39 40 syl2an2r ⊢ ( ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) ∧ 𝑦 ∈ ω ) → ( 𝐹 ‘ ( 𝑔 ‘ suc 𝑦 ) ) = ( 𝐴 ∖ ( 𝑔 ‘ suc 𝑦 ) ) )
42 35 41 sseq12d ⊢ ( ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) ∧ 𝑦 ∈ ω ) → ( ( 𝐹 ‘ ( 𝑔 ‘ 𝑦 ) ) ⊆ ( 𝐹 ‘ ( 𝑔 ‘ suc 𝑦 ) ) ↔ ( 𝐴 ∖ ( 𝑔 ‘ 𝑦 ) ) ⊆ ( 𝐴 ∖ ( 𝑔 ‘ suc 𝑦 ) ) ) )
43 31 42 syl5ibr ⊢ ( ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) ∧ 𝑦 ∈ ω ) → ( ( 𝑔 ‘ suc 𝑦 ) ⊆ ( 𝑔 ‘ 𝑦 ) → ( 𝐹 ‘ ( 𝑔 ‘ 𝑦 ) ) ⊆ ( 𝐹 ‘ ( 𝑔 ‘ suc 𝑦 ) ) ) )
44 fvco3 ⊢ ( ( 𝑔 : ω ⟶ 𝒫 𝐴 ∧ 𝑦 ∈ ω ) → ( ( 𝐹 ∘ 𝑔 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑔 ‘ 𝑦 ) ) )
45 13 44 sylan ⊢ ( ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) ∧ 𝑦 ∈ ω ) → ( ( 𝐹 ∘ 𝑔 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑔 ‘ 𝑦 ) ) )
46 fvco3 ⊢ ( ( 𝑔 : ω ⟶ 𝒫 𝐴 ∧ suc 𝑦 ∈ ω ) → ( ( 𝐹 ∘ 𝑔 ) ‘ suc 𝑦 ) = ( 𝐹 ‘ ( 𝑔 ‘ suc 𝑦 ) ) )
47 13 36 46 syl2an ⊢ ( ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) ∧ 𝑦 ∈ ω ) → ( ( 𝐹 ∘ 𝑔 ) ‘ suc 𝑦 ) = ( 𝐹 ‘ ( 𝑔 ‘ suc 𝑦 ) ) )
48 45 47 sseq12d ⊢ ( ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) ∧ 𝑦 ∈ ω ) → ( ( ( 𝐹 ∘ 𝑔 ) ‘ 𝑦 ) ⊆ ( ( 𝐹 ∘ 𝑔 ) ‘ suc 𝑦 ) ↔ ( 𝐹 ‘ ( 𝑔 ‘ 𝑦 ) ) ⊆ ( 𝐹 ‘ ( 𝑔 ‘ suc 𝑦 ) ) ) )
49 43 48 sylibrd ⊢ ( ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) ∧ 𝑦 ∈ ω ) → ( ( 𝑔 ‘ suc 𝑦 ) ⊆ ( 𝑔 ‘ 𝑦 ) → ( ( 𝐹 ∘ 𝑔 ) ‘ 𝑦 ) ⊆ ( ( 𝐹 ∘ 𝑔 ) ‘ suc 𝑦 ) ) )
50 49 ralimdva ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( ∀ 𝑦 ∈ ω ( 𝑔 ‘ suc 𝑦 ) ⊆ ( 𝑔 ‘ 𝑦 ) → ∀ 𝑦 ∈ ω ( ( 𝐹 ∘ 𝑔 ) ‘ 𝑦 ) ⊆ ( ( 𝐹 ∘ 𝑔 ) ‘ suc 𝑦 ) ) )
51 12 ffnd ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → 𝐹 Fn 𝒫 𝐴 )
52 imassrn ⊢ ( 𝐹 “ ran 𝑔 ) ⊆ ran 𝐹
53 12 frnd ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ran 𝐹 ⊆ 𝒫 𝐴 )
54 52 53 sstrid ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( 𝐹 “ ran 𝑔 ) ⊆ 𝒫 𝐴 )
55 fnfvima ⊢ ( ( 𝐹 Fn 𝒫 𝐴 ∧ ( 𝐹 “ ran 𝑔 ) ⊆ 𝒫 𝐴 ∧ ∪ ( 𝐹 “ ran 𝑔 ) ∈ ( 𝐹 “ ran 𝑔 ) ) → ( 𝐹 ‘ ∪ ( 𝐹 “ ran 𝑔 ) ) ∈ ( 𝐹 “ ( 𝐹 “ ran 𝑔 ) ) )
56 55 3expia ⊢ ( ( 𝐹 Fn 𝒫 𝐴 ∧ ( 𝐹 “ ran 𝑔 ) ⊆ 𝒫 𝐴 ) → ( ∪ ( 𝐹 “ ran 𝑔 ) ∈ ( 𝐹 “ ran 𝑔 ) → ( 𝐹 ‘ ∪ ( 𝐹 “ ran 𝑔 ) ) ∈ ( 𝐹 “ ( 𝐹 “ ran 𝑔 ) ) ) )
57 51 54 56 syl2anc ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( ∪ ( 𝐹 “ ran 𝑔 ) ∈ ( 𝐹 “ ran 𝑔 ) → ( 𝐹 ‘ ∪ ( 𝐹 “ ran 𝑔 ) ) ∈ ( 𝐹 “ ( 𝐹 “ ran 𝑔 ) ) ) )
58 incom ⊢ ( dom 𝐹 ∩ ran 𝑔 ) = ( ran 𝑔 ∩ dom 𝐹 )
59 13 frnd ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ran 𝑔 ⊆ 𝒫 𝐴 )
60 12 fdmd ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → dom 𝐹 = 𝒫 𝐴 )
61 59 60 sseqtrrd ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ran 𝑔 ⊆ dom 𝐹 )
62 df-ss ⊢ ( ran 𝑔 ⊆ dom 𝐹 ↔ ( ran 𝑔 ∩ dom 𝐹 ) = ran 𝑔 )
63 61 62 sylib ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( ran 𝑔 ∩ dom 𝐹 ) = ran 𝑔 )
64 58 63 eqtrid ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( dom 𝐹 ∩ ran 𝑔 ) = ran 𝑔 )
65 13 fdmd ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → dom 𝑔 = ω )
66 peano1 ⊢ ∅ ∈ ω
67 ne0i ⊢ ( ∅ ∈ ω → ω ≠ ∅ )
68 66 67 mp1i ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ω ≠ ∅ )
69 65 68 eqnetrd ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → dom 𝑔 ≠ ∅ )
70 dm0rn0 ⊢ ( dom 𝑔 = ∅ ↔ ran 𝑔 = ∅ )
71 70 necon3bii ⊢ ( dom 𝑔 ≠ ∅ ↔ ran 𝑔 ≠ ∅ )
72 69 71 sylib ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ran 𝑔 ≠ ∅ )
73 64 72 eqnetrd ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( dom 𝐹 ∩ ran 𝑔 ) ≠ ∅ )
74 imadisj ⊢ ( ( 𝐹 “ ran 𝑔 ) = ∅ ↔ ( dom 𝐹 ∩ ran 𝑔 ) = ∅ )
75 74 necon3bii ⊢ ( ( 𝐹 “ ran 𝑔 ) ≠ ∅ ↔ ( dom 𝐹 ∩ ran 𝑔 ) ≠ ∅ )
76 73 75 sylibr ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( 𝐹 “ ran 𝑔 ) ≠ ∅ )
77 1 isf34lem4 ⊢ ( ( 𝐴 ∈ V ∧ ( ( 𝐹 “ ran 𝑔 ) ⊆ 𝒫 𝐴 ∧ ( 𝐹 “ ran 𝑔 ) ≠ ∅ ) ) → ( 𝐹 ‘ ∪ ( 𝐹 “ ran 𝑔 ) ) = ∩ ( 𝐹 “ ( 𝐹 “ ran 𝑔 ) ) )
78 10 54 76 77 syl12anc ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( 𝐹 ‘ ∪ ( 𝐹 “ ran 𝑔 ) ) = ∩ ( 𝐹 “ ( 𝐹 “ ran 𝑔 ) ) )
79 1 isf34lem3 ⊢ ( ( 𝐴 ∈ V ∧ ran 𝑔 ⊆ 𝒫 𝐴 ) → ( 𝐹 “ ( 𝐹 “ ran 𝑔 ) ) = ran 𝑔 )
80 10 59 79 syl2anc ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( 𝐹 “ ( 𝐹 “ ran 𝑔 ) ) = ran 𝑔 )
81 80 inteqd ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ∩ ( 𝐹 “ ( 𝐹 “ ran 𝑔 ) ) = ∩ ran 𝑔 )
82 78 81 eqtrd ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( 𝐹 ‘ ∪ ( 𝐹 “ ran 𝑔 ) ) = ∩ ran 𝑔 )
83 82 80 eleq12d ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( ( 𝐹 ‘ ∪ ( 𝐹 “ ran 𝑔 ) ) ∈ ( 𝐹 “ ( 𝐹 “ ran 𝑔 ) ) ↔ ∩ ran 𝑔 ∈ ran 𝑔 ) )
84 57 83 sylibd ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( ∪ ( 𝐹 “ ran 𝑔 ) ∈ ( 𝐹 “ ran 𝑔 ) → ∩ ran 𝑔 ∈ ran 𝑔 ) )
85 50 84 imim12d ⊢ ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( ( ∀ 𝑦 ∈ ω ( ( 𝐹 ∘ 𝑔 ) ‘ 𝑦 ) ⊆ ( ( 𝐹 ∘ 𝑔 ) ‘ suc 𝑦 ) → ∪ ( 𝐹 “ ran 𝑔 ) ∈ ( 𝐹 “ ran 𝑔 ) ) → ( ∀ 𝑦 ∈ ω ( 𝑔 ‘ suc 𝑦 ) ⊆ ( 𝑔 ‘ 𝑦 ) → ∩ ran 𝑔 ∈ ran 𝑔 ) ) )
86 30 85 sylcom ⊢ ( ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑦 ∈ ω ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ suc 𝑦 ) → ∪ ran 𝑓 ∈ ran 𝑓 ) → ( 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) → ( ∀ 𝑦 ∈ ω ( 𝑔 ‘ suc 𝑦 ) ⊆ ( 𝑔 ‘ 𝑦 ) → ∩ ran 𝑔 ∈ ran 𝑔 ) ) )
87 86 ralrimiv ⊢ ( ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑦 ∈ ω ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ suc 𝑦 ) → ∪ ran 𝑓 ∈ ran 𝑓 ) → ∀ 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑦 ∈ ω ( 𝑔 ‘ suc 𝑦 ) ⊆ ( 𝑔 ‘ 𝑦 ) → ∩ ran 𝑔 ∈ ran 𝑔 ) )
88 isfin3-3 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinIII ↔ ∀ 𝑔 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑦 ∈ ω ( 𝑔 ‘ suc 𝑦 ) ⊆ ( 𝑔 ‘ 𝑦 ) → ∩ ran 𝑔 ∈ ran 𝑔 ) ) )
89 87 88 syl5ibr ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑦 ∈ ω ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ suc 𝑦 ) → ∪ ran 𝑓 ∈ ran 𝑓 ) → 𝐴 ∈ FinIII ) )
90 6 89 impbid2 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinIII ↔ ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑦 ∈ ω ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ suc 𝑦 ) → ∪ ran 𝑓 ∈ ran 𝑓 ) ) )