| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elmapi 8890 | . . . 4
⊢ (𝑓 ∈ (𝒫 𝐴 ↑m ω)
→ 𝑓:ω⟶𝒫 𝐴) | 
| 2 |  | compss.a | . . . . . 6
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) | 
| 3 | 2 | isf34lem7 10420 | . . . . 5
⊢ ((𝐴 ∈ FinIII ∧
𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦)) → ∪ ran
𝑓 ∈ ran 𝑓) | 
| 4 | 3 | 3expia 1121 | . . . 4
⊢ ((𝐴 ∈ FinIII ∧
𝑓:ω⟶𝒫
𝐴) → (∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓)) | 
| 5 | 1, 4 | sylan2 593 | . . 3
⊢ ((𝐴 ∈ FinIII ∧
𝑓 ∈ (𝒫 𝐴 ↑m ω))
→ (∀𝑦 ∈
ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓)) | 
| 6 | 5 | ralrimiva 3145 | . 2
⊢ (𝐴 ∈ FinIII →
∀𝑓 ∈ (𝒫
𝐴 ↑m
ω)(∀𝑦 ∈
ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓)) | 
| 7 |  | elmapex 8889 | . . . . . . . . . . 11
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝒫 𝐴 ∈
V ∧ ω ∈ V)) | 
| 8 | 7 | simpld 494 | . . . . . . . . . 10
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ 𝒫 𝐴 ∈
V) | 
| 9 |  | pwexb 7787 | . . . . . . . . . 10
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V) | 
| 10 | 8, 9 | sylibr 234 | . . . . . . . . 9
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ 𝐴 ∈
V) | 
| 11 | 2 | isf34lem2 10414 | . . . . . . . . 9
⊢ (𝐴 ∈ V → 𝐹:𝒫 𝐴⟶𝒫 𝐴) | 
| 12 | 10, 11 | syl 17 | . . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ 𝐹:𝒫 𝐴⟶𝒫 𝐴) | 
| 13 |  | elmapi 8890 | . . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ 𝑔:ω⟶𝒫 𝐴) | 
| 14 |  | fco 6759 | . . . . . . . 8
⊢ ((𝐹:𝒫 𝐴⟶𝒫 𝐴 ∧ 𝑔:ω⟶𝒫 𝐴) → (𝐹 ∘ 𝑔):ω⟶𝒫 𝐴) | 
| 15 | 12, 13, 14 | syl2anc 584 | . . . . . . 7
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝐹 ∘ 𝑔):ω⟶𝒫 𝐴) | 
| 16 |  | elmapg 8880 | . . . . . . . 8
⊢
((𝒫 𝐴 ∈
V ∧ ω ∈ V) → ((𝐹 ∘ 𝑔) ∈ (𝒫 𝐴 ↑m ω) ↔ (𝐹 ∘ 𝑔):ω⟶𝒫 𝐴)) | 
| 17 | 7, 16 | syl 17 | . . . . . . 7
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ((𝐹 ∘ 𝑔) ∈ (𝒫 𝐴 ↑m ω)
↔ (𝐹 ∘ 𝑔):ω⟶𝒫 𝐴)) | 
| 18 | 15, 17 | mpbird 257 | . . . . . 6
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝐹 ∘ 𝑔) ∈ (𝒫 𝐴 ↑m
ω)) | 
| 19 |  | fveq1 6904 | . . . . . . . . . 10
⊢ (𝑓 = (𝐹 ∘ 𝑔) → (𝑓‘𝑦) = ((𝐹 ∘ 𝑔)‘𝑦)) | 
| 20 |  | fveq1 6904 | . . . . . . . . . 10
⊢ (𝑓 = (𝐹 ∘ 𝑔) → (𝑓‘suc 𝑦) = ((𝐹 ∘ 𝑔)‘suc 𝑦)) | 
| 21 | 19, 20 | sseq12d 4016 | . . . . . . . . 9
⊢ (𝑓 = (𝐹 ∘ 𝑔) → ((𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) ↔ ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦))) | 
| 22 | 21 | ralbidv 3177 | . . . . . . . 8
⊢ (𝑓 = (𝐹 ∘ 𝑔) → (∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) ↔ ∀𝑦 ∈ ω ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦))) | 
| 23 |  | rneq 5946 | . . . . . . . . . . 11
⊢ (𝑓 = (𝐹 ∘ 𝑔) → ran 𝑓 = ran (𝐹 ∘ 𝑔)) | 
| 24 |  | rnco2 6272 | . . . . . . . . . . 11
⊢ ran
(𝐹 ∘ 𝑔) = (𝐹 “ ran 𝑔) | 
| 25 | 23, 24 | eqtrdi 2792 | . . . . . . . . . 10
⊢ (𝑓 = (𝐹 ∘ 𝑔) → ran 𝑓 = (𝐹 “ ran 𝑔)) | 
| 26 | 25 | unieqd 4919 | . . . . . . . . 9
⊢ (𝑓 = (𝐹 ∘ 𝑔) → ∪ ran
𝑓 = ∪ (𝐹
“ ran 𝑔)) | 
| 27 | 26, 25 | eleq12d 2834 | . . . . . . . 8
⊢ (𝑓 = (𝐹 ∘ 𝑔) → (∪ ran
𝑓 ∈ ran 𝑓 ↔ ∪ (𝐹
“ ran 𝑔) ∈
(𝐹 “ ran 𝑔))) | 
| 28 | 22, 27 | imbi12d 344 | . . . . . . 7
⊢ (𝑓 = (𝐹 ∘ 𝑔) → ((∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓) ↔ (∀𝑦 ∈ ω ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦) → ∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔)))) | 
| 29 | 28 | rspccv 3618 | . . . . . 6
⊢
(∀𝑓 ∈
(𝒫 𝐴
↑m ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓) → ((𝐹 ∘ 𝑔) ∈ (𝒫 𝐴 ↑m ω) →
(∀𝑦 ∈ ω
((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦) → ∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔)))) | 
| 30 | 18, 29 | syl5 34 | . . . . 5
⊢
(∀𝑓 ∈
(𝒫 𝐴
↑m ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓) → (𝑔 ∈ (𝒫 𝐴 ↑m ω) →
(∀𝑦 ∈ ω
((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦) → ∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔)))) | 
| 31 |  | sscon 4142 | . . . . . . . . 9
⊢ ((𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → (𝐴 ∖ (𝑔‘𝑦)) ⊆ (𝐴 ∖ (𝑔‘suc 𝑦))) | 
| 32 | 13 | ffvelcdmda 7103 | . . . . . . . . . . . 12
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ (𝑔‘𝑦) ∈ 𝒫 𝐴) | 
| 33 | 32 | elpwid 4608 | . . . . . . . . . . 11
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ (𝑔‘𝑦) ⊆ 𝐴) | 
| 34 | 2 | isf34lem1 10413 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (𝑔‘𝑦) ⊆ 𝐴) → (𝐹‘(𝑔‘𝑦)) = (𝐴 ∖ (𝑔‘𝑦))) | 
| 35 | 10, 33, 34 | syl2an2r 685 | . . . . . . . . . 10
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ (𝐹‘(𝑔‘𝑦)) = (𝐴 ∖ (𝑔‘𝑦))) | 
| 36 |  | peano2 7913 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ω → suc 𝑦 ∈
ω) | 
| 37 |  | ffvelcdm 7100 | . . . . . . . . . . . . 13
⊢ ((𝑔:ω⟶𝒫 𝐴 ∧ suc 𝑦 ∈ ω) → (𝑔‘suc 𝑦) ∈ 𝒫 𝐴) | 
| 38 | 13, 36, 37 | syl2an 596 | . . . . . . . . . . . 12
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ (𝑔‘suc 𝑦) ∈ 𝒫 𝐴) | 
| 39 | 38 | elpwid 4608 | . . . . . . . . . . 11
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ (𝑔‘suc 𝑦) ⊆ 𝐴) | 
| 40 | 2 | isf34lem1 10413 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (𝑔‘suc 𝑦) ⊆ 𝐴) → (𝐹‘(𝑔‘suc 𝑦)) = (𝐴 ∖ (𝑔‘suc 𝑦))) | 
| 41 | 10, 39, 40 | syl2an2r 685 | . . . . . . . . . 10
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ (𝐹‘(𝑔‘suc 𝑦)) = (𝐴 ∖ (𝑔‘suc 𝑦))) | 
| 42 | 35, 41 | sseq12d 4016 | . . . . . . . . 9
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ ((𝐹‘(𝑔‘𝑦)) ⊆ (𝐹‘(𝑔‘suc 𝑦)) ↔ (𝐴 ∖ (𝑔‘𝑦)) ⊆ (𝐴 ∖ (𝑔‘suc 𝑦)))) | 
| 43 | 31, 42 | imbitrrid 246 | . . . . . . . 8
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ ((𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → (𝐹‘(𝑔‘𝑦)) ⊆ (𝐹‘(𝑔‘suc 𝑦)))) | 
| 44 |  | fvco3 7007 | . . . . . . . . . 10
⊢ ((𝑔:ω⟶𝒫 𝐴 ∧ 𝑦 ∈ ω) → ((𝐹 ∘ 𝑔)‘𝑦) = (𝐹‘(𝑔‘𝑦))) | 
| 45 | 13, 44 | sylan 580 | . . . . . . . . 9
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ ((𝐹 ∘ 𝑔)‘𝑦) = (𝐹‘(𝑔‘𝑦))) | 
| 46 |  | fvco3 7007 | . . . . . . . . . 10
⊢ ((𝑔:ω⟶𝒫 𝐴 ∧ suc 𝑦 ∈ ω) → ((𝐹 ∘ 𝑔)‘suc 𝑦) = (𝐹‘(𝑔‘suc 𝑦))) | 
| 47 | 13, 36, 46 | syl2an 596 | . . . . . . . . 9
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ ((𝐹 ∘ 𝑔)‘suc 𝑦) = (𝐹‘(𝑔‘suc 𝑦))) | 
| 48 | 45, 47 | sseq12d 4016 | . . . . . . . 8
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ (((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦) ↔ (𝐹‘(𝑔‘𝑦)) ⊆ (𝐹‘(𝑔‘suc 𝑦)))) | 
| 49 | 43, 48 | sylibrd 259 | . . . . . . 7
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ ((𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦))) | 
| 50 | 49 | ralimdva 3166 | . . . . . 6
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (∀𝑦 ∈
ω (𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → ∀𝑦 ∈ ω ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦))) | 
| 51 | 12 | ffnd 6736 | . . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ 𝐹 Fn 𝒫 𝐴) | 
| 52 |  | imassrn 6088 | . . . . . . . . 9
⊢ (𝐹 “ ran 𝑔) ⊆ ran 𝐹 | 
| 53 | 12 | frnd 6743 | . . . . . . . . 9
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ran 𝐹 ⊆
𝒫 𝐴) | 
| 54 | 52, 53 | sstrid 3994 | . . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝐹 “ ran 𝑔) ⊆ 𝒫 𝐴) | 
| 55 |  | fnfvima 7254 | . . . . . . . . 9
⊢ ((𝐹 Fn 𝒫 𝐴 ∧ (𝐹 “ ran 𝑔) ⊆ 𝒫 𝐴 ∧ ∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔)) → (𝐹‘∪ (𝐹 “ ran 𝑔)) ∈ (𝐹 “ (𝐹 “ ran 𝑔))) | 
| 56 | 55 | 3expia 1121 | . . . . . . . 8
⊢ ((𝐹 Fn 𝒫 𝐴 ∧ (𝐹 “ ran 𝑔) ⊆ 𝒫 𝐴) → (∪
(𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔) → (𝐹‘∪ (𝐹 “ ran 𝑔)) ∈ (𝐹 “ (𝐹 “ ran 𝑔)))) | 
| 57 | 51, 54, 56 | syl2anc 584 | . . . . . . 7
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔) → (𝐹‘∪ (𝐹 “ ran 𝑔)) ∈ (𝐹 “ (𝐹 “ ran 𝑔)))) | 
| 58 |  | incom 4208 | . . . . . . . . . . . . 13
⊢ (dom
𝐹 ∩ ran 𝑔) = (ran 𝑔 ∩ dom 𝐹) | 
| 59 | 13 | frnd 6743 | . . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ran 𝑔 ⊆
𝒫 𝐴) | 
| 60 | 12 | fdmd 6745 | . . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ dom 𝐹 = 𝒫
𝐴) | 
| 61 | 59, 60 | sseqtrrd 4020 | . . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ran 𝑔 ⊆ dom
𝐹) | 
| 62 |  | dfss2 3968 | . . . . . . . . . . . . . 14
⊢ (ran
𝑔 ⊆ dom 𝐹 ↔ (ran 𝑔 ∩ dom 𝐹) = ran 𝑔) | 
| 63 | 61, 62 | sylib 218 | . . . . . . . . . . . . 13
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (ran 𝑔 ∩ dom
𝐹) = ran 𝑔) | 
| 64 | 58, 63 | eqtrid 2788 | . . . . . . . . . . . 12
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (dom 𝐹 ∩ ran
𝑔) = ran 𝑔) | 
| 65 | 13 | fdmd 6745 | . . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ dom 𝑔 =
ω) | 
| 66 |  | peano1 7911 | . . . . . . . . . . . . . . 15
⊢ ∅
∈ ω | 
| 67 |  | ne0i 4340 | . . . . . . . . . . . . . . 15
⊢ (∅
∈ ω → ω ≠ ∅) | 
| 68 | 66, 67 | mp1i 13 | . . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ω ≠ ∅) | 
| 69 | 65, 68 | eqnetrd 3007 | . . . . . . . . . . . . 13
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ dom 𝑔 ≠
∅) | 
| 70 |  | dm0rn0 5934 | . . . . . . . . . . . . . 14
⊢ (dom
𝑔 = ∅ ↔ ran
𝑔 =
∅) | 
| 71 | 70 | necon3bii 2992 | . . . . . . . . . . . . 13
⊢ (dom
𝑔 ≠ ∅ ↔ ran
𝑔 ≠
∅) | 
| 72 | 69, 71 | sylib 218 | . . . . . . . . . . . 12
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ran 𝑔 ≠
∅) | 
| 73 | 64, 72 | eqnetrd 3007 | . . . . . . . . . . 11
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (dom 𝐹 ∩ ran
𝑔) ≠
∅) | 
| 74 |  | imadisj 6097 | . . . . . . . . . . . 12
⊢ ((𝐹 “ ran 𝑔) = ∅ ↔ (dom 𝐹 ∩ ran 𝑔) = ∅) | 
| 75 | 74 | necon3bii 2992 | . . . . . . . . . . 11
⊢ ((𝐹 “ ran 𝑔) ≠ ∅ ↔ (dom 𝐹 ∩ ran 𝑔) ≠ ∅) | 
| 76 | 73, 75 | sylibr 234 | . . . . . . . . . 10
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝐹 “ ran 𝑔) ≠ ∅) | 
| 77 | 2 | isf34lem4 10418 | . . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ ((𝐹 “ ran 𝑔) ⊆ 𝒫 𝐴 ∧ (𝐹 “ ran 𝑔) ≠ ∅)) → (𝐹‘∪ (𝐹 “ ran 𝑔)) = ∩ (𝐹 “ (𝐹 “ ran 𝑔))) | 
| 78 | 10, 54, 76, 77 | syl12anc 836 | . . . . . . . . 9
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝐹‘∪ (𝐹
“ ran 𝑔)) = ∩ (𝐹
“ (𝐹 “ ran
𝑔))) | 
| 79 | 2 | isf34lem3 10416 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ ran 𝑔 ⊆ 𝒫 𝐴) → (𝐹 “ (𝐹 “ ran 𝑔)) = ran 𝑔) | 
| 80 | 10, 59, 79 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝐹 “ (𝐹 “ ran 𝑔)) = ran 𝑔) | 
| 81 | 80 | inteqd 4950 | . . . . . . . . 9
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ∩ (𝐹 “ (𝐹 “ ran 𝑔)) = ∩ ran 𝑔) | 
| 82 | 78, 81 | eqtrd 2776 | . . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝐹‘∪ (𝐹
“ ran 𝑔)) = ∩ ran 𝑔) | 
| 83 | 82, 80 | eleq12d 2834 | . . . . . . 7
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ((𝐹‘∪ (𝐹
“ ran 𝑔)) ∈
(𝐹 “ (𝐹 “ ran 𝑔)) ↔ ∩ ran
𝑔 ∈ ran 𝑔)) | 
| 84 | 57, 83 | sylibd 239 | . . . . . 6
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔) → ∩ ran
𝑔 ∈ ran 𝑔)) | 
| 85 | 50, 84 | imim12d 81 | . . . . 5
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ((∀𝑦 ∈
ω ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦) → ∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔)) → (∀𝑦 ∈ ω (𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → ∩ ran
𝑔 ∈ ran 𝑔))) | 
| 86 | 30, 85 | sylcom 30 | . . . 4
⊢
(∀𝑓 ∈
(𝒫 𝐴
↑m ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓) → (𝑔 ∈ (𝒫 𝐴 ↑m ω) →
(∀𝑦 ∈ ω
(𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → ∩ ran
𝑔 ∈ ran 𝑔))) | 
| 87 | 86 | ralrimiv 3144 | . . 3
⊢
(∀𝑓 ∈
(𝒫 𝐴
↑m ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓) → ∀𝑔 ∈ (𝒫 𝐴 ↑m
ω)(∀𝑦 ∈
ω (𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → ∩ ran
𝑔 ∈ ran 𝑔)) | 
| 88 |  | isfin3-3 10409 | . . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔
∀𝑔 ∈ (𝒫
𝐴 ↑m
ω)(∀𝑦 ∈
ω (𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → ∩ ran
𝑔 ∈ ran 𝑔))) | 
| 89 | 87, 88 | imbitrrid 246 | . 2
⊢ (𝐴 ∈ 𝑉 → (∀𝑓 ∈ (𝒫 𝐴 ↑m ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓) → 𝐴 ∈ FinIII)) | 
| 90 | 6, 89 | impbid2 226 | 1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔
∀𝑓 ∈ (𝒫
𝐴 ↑m
ω)(∀𝑦 ∈
ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓))) |