Step | Hyp | Ref
| Expression |
1 | | elmapi 8637 |
. . . 4
⊢ (𝑓 ∈ (𝒫 𝐴 ↑m ω)
→ 𝑓:ω⟶𝒫 𝐴) |
2 | | compss.a |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) |
3 | 2 | isf34lem7 10135 |
. . . . 5
⊢ ((𝐴 ∈ FinIII ∧
𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦)) → ∪ ran
𝑓 ∈ ran 𝑓) |
4 | 3 | 3expia 1120 |
. . . 4
⊢ ((𝐴 ∈ FinIII ∧
𝑓:ω⟶𝒫
𝐴) → (∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓)) |
5 | 1, 4 | sylan2 593 |
. . 3
⊢ ((𝐴 ∈ FinIII ∧
𝑓 ∈ (𝒫 𝐴 ↑m ω))
→ (∀𝑦 ∈
ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓)) |
6 | 5 | ralrimiva 3103 |
. 2
⊢ (𝐴 ∈ FinIII →
∀𝑓 ∈ (𝒫
𝐴 ↑m
ω)(∀𝑦 ∈
ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓)) |
7 | | elmapex 8636 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝒫 𝐴 ∈
V ∧ ω ∈ V)) |
8 | 7 | simpld 495 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ 𝒫 𝐴 ∈
V) |
9 | | pwexb 7616 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V) |
10 | 8, 9 | sylibr 233 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ 𝐴 ∈
V) |
11 | 2 | isf34lem2 10129 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → 𝐹:𝒫 𝐴⟶𝒫 𝐴) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ 𝐹:𝒫 𝐴⟶𝒫 𝐴) |
13 | | elmapi 8637 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ 𝑔:ω⟶𝒫 𝐴) |
14 | | fco 6624 |
. . . . . . . 8
⊢ ((𝐹:𝒫 𝐴⟶𝒫 𝐴 ∧ 𝑔:ω⟶𝒫 𝐴) → (𝐹 ∘ 𝑔):ω⟶𝒫 𝐴) |
15 | 12, 13, 14 | syl2anc 584 |
. . . . . . 7
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝐹 ∘ 𝑔):ω⟶𝒫 𝐴) |
16 | | elmapg 8628 |
. . . . . . . 8
⊢
((𝒫 𝐴 ∈
V ∧ ω ∈ V) → ((𝐹 ∘ 𝑔) ∈ (𝒫 𝐴 ↑m ω) ↔ (𝐹 ∘ 𝑔):ω⟶𝒫 𝐴)) |
17 | 7, 16 | syl 17 |
. . . . . . 7
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ((𝐹 ∘ 𝑔) ∈ (𝒫 𝐴 ↑m ω)
↔ (𝐹 ∘ 𝑔):ω⟶𝒫 𝐴)) |
18 | 15, 17 | mpbird 256 |
. . . . . 6
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝐹 ∘ 𝑔) ∈ (𝒫 𝐴 ↑m
ω)) |
19 | | fveq1 6773 |
. . . . . . . . . 10
⊢ (𝑓 = (𝐹 ∘ 𝑔) → (𝑓‘𝑦) = ((𝐹 ∘ 𝑔)‘𝑦)) |
20 | | fveq1 6773 |
. . . . . . . . . 10
⊢ (𝑓 = (𝐹 ∘ 𝑔) → (𝑓‘suc 𝑦) = ((𝐹 ∘ 𝑔)‘suc 𝑦)) |
21 | 19, 20 | sseq12d 3954 |
. . . . . . . . 9
⊢ (𝑓 = (𝐹 ∘ 𝑔) → ((𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) ↔ ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦))) |
22 | 21 | ralbidv 3112 |
. . . . . . . 8
⊢ (𝑓 = (𝐹 ∘ 𝑔) → (∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) ↔ ∀𝑦 ∈ ω ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦))) |
23 | | rneq 5845 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝐹 ∘ 𝑔) → ran 𝑓 = ran (𝐹 ∘ 𝑔)) |
24 | | rnco2 6157 |
. . . . . . . . . . 11
⊢ ran
(𝐹 ∘ 𝑔) = (𝐹 “ ran 𝑔) |
25 | 23, 24 | eqtrdi 2794 |
. . . . . . . . . 10
⊢ (𝑓 = (𝐹 ∘ 𝑔) → ran 𝑓 = (𝐹 “ ran 𝑔)) |
26 | 25 | unieqd 4853 |
. . . . . . . . 9
⊢ (𝑓 = (𝐹 ∘ 𝑔) → ∪ ran
𝑓 = ∪ (𝐹
“ ran 𝑔)) |
27 | 26, 25 | eleq12d 2833 |
. . . . . . . 8
⊢ (𝑓 = (𝐹 ∘ 𝑔) → (∪ ran
𝑓 ∈ ran 𝑓 ↔ ∪ (𝐹
“ ran 𝑔) ∈
(𝐹 “ ran 𝑔))) |
28 | 22, 27 | imbi12d 345 |
. . . . . . 7
⊢ (𝑓 = (𝐹 ∘ 𝑔) → ((∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓) ↔ (∀𝑦 ∈ ω ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦) → ∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔)))) |
29 | 28 | rspccv 3558 |
. . . . . 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 4073 |
. . . . . . . . 9
⊢ ((𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → (𝐴 ∖ (𝑔‘𝑦)) ⊆ (𝐴 ∖ (𝑔‘suc 𝑦))) |
32 | 13 | ffvelrnda 6961 |
. . . . . . . . . . . 12
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ (𝑔‘𝑦) ∈ 𝒫 𝐴) |
33 | 32 | elpwid 4544 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ (𝑔‘𝑦) ⊆ 𝐴) |
34 | 2 | isf34lem1 10128 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (𝑔‘𝑦) ⊆ 𝐴) → (𝐹‘(𝑔‘𝑦)) = (𝐴 ∖ (𝑔‘𝑦))) |
35 | 10, 33, 34 | syl2an2r 682 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ (𝐹‘(𝑔‘𝑦)) = (𝐴 ∖ (𝑔‘𝑦))) |
36 | | peano2 7737 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ω → suc 𝑦 ∈
ω) |
37 | | ffvelrn 6959 |
. . . . . . . . . . . . 13
⊢ ((𝑔:ω⟶𝒫 𝐴 ∧ suc 𝑦 ∈ ω) → (𝑔‘suc 𝑦) ∈ 𝒫 𝐴) |
38 | 13, 36, 37 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ (𝑔‘suc 𝑦) ∈ 𝒫 𝐴) |
39 | 38 | elpwid 4544 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ (𝑔‘suc 𝑦) ⊆ 𝐴) |
40 | 2 | isf34lem1 10128 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (𝑔‘suc 𝑦) ⊆ 𝐴) → (𝐹‘(𝑔‘suc 𝑦)) = (𝐴 ∖ (𝑔‘suc 𝑦))) |
41 | 10, 39, 40 | syl2an2r 682 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ (𝐹‘(𝑔‘suc 𝑦)) = (𝐴 ∖ (𝑔‘suc 𝑦))) |
42 | 35, 41 | sseq12d 3954 |
. . . . . . . . 9
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ ((𝐹‘(𝑔‘𝑦)) ⊆ (𝐹‘(𝑔‘suc 𝑦)) ↔ (𝐴 ∖ (𝑔‘𝑦)) ⊆ (𝐴 ∖ (𝑔‘suc 𝑦)))) |
43 | 31, 42 | syl5ibr 245 |
. . . . . . . 8
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ ((𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → (𝐹‘(𝑔‘𝑦)) ⊆ (𝐹‘(𝑔‘suc 𝑦)))) |
44 | | fvco3 6867 |
. . . . . . . . . 10
⊢ ((𝑔:ω⟶𝒫 𝐴 ∧ 𝑦 ∈ ω) → ((𝐹 ∘ 𝑔)‘𝑦) = (𝐹‘(𝑔‘𝑦))) |
45 | 13, 44 | sylan 580 |
. . . . . . . . 9
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ ((𝐹 ∘ 𝑔)‘𝑦) = (𝐹‘(𝑔‘𝑦))) |
46 | | fvco3 6867 |
. . . . . . . . . 10
⊢ ((𝑔:ω⟶𝒫 𝐴 ∧ suc 𝑦 ∈ ω) → ((𝐹 ∘ 𝑔)‘suc 𝑦) = (𝐹‘(𝑔‘suc 𝑦))) |
47 | 13, 36, 46 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ ((𝐹 ∘ 𝑔)‘suc 𝑦) = (𝐹‘(𝑔‘suc 𝑦))) |
48 | 45, 47 | sseq12d 3954 |
. . . . . . . 8
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ (((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦) ↔ (𝐹‘(𝑔‘𝑦)) ⊆ (𝐹‘(𝑔‘suc 𝑦)))) |
49 | 43, 48 | sylibrd 258 |
. . . . . . 7
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑m ω)
∧ 𝑦 ∈ ω)
→ ((𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦))) |
50 | 49 | ralimdva 3108 |
. . . . . 6
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (∀𝑦 ∈
ω (𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → ∀𝑦 ∈ ω ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦))) |
51 | 12 | ffnd 6601 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ 𝐹 Fn 𝒫 𝐴) |
52 | | imassrn 5980 |
. . . . . . . . 9
⊢ (𝐹 “ ran 𝑔) ⊆ ran 𝐹 |
53 | 12 | frnd 6608 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ran 𝐹 ⊆
𝒫 𝐴) |
54 | 52, 53 | sstrid 3932 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝐹 “ ran 𝑔) ⊆ 𝒫 𝐴) |
55 | | fnfvima 7109 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝒫 𝐴 ∧ (𝐹 “ ran 𝑔) ⊆ 𝒫 𝐴 ∧ ∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔)) → (𝐹‘∪ (𝐹 “ ran 𝑔)) ∈ (𝐹 “ (𝐹 “ ran 𝑔))) |
56 | 55 | 3expia 1120 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝒫 𝐴 ∧ (𝐹 “ ran 𝑔) ⊆ 𝒫 𝐴) → (∪
(𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔) → (𝐹‘∪ (𝐹 “ ran 𝑔)) ∈ (𝐹 “ (𝐹 “ ran 𝑔)))) |
57 | 51, 54, 56 | syl2anc 584 |
. . . . . . 7
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔) → (𝐹‘∪ (𝐹 “ ran 𝑔)) ∈ (𝐹 “ (𝐹 “ ran 𝑔)))) |
58 | | incom 4135 |
. . . . . . . . . . . . 13
⊢ (dom
𝐹 ∩ ran 𝑔) = (ran 𝑔 ∩ dom 𝐹) |
59 | 13 | frnd 6608 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ran 𝑔 ⊆
𝒫 𝐴) |
60 | 12 | fdmd 6611 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ dom 𝐹 = 𝒫
𝐴) |
61 | 59, 60 | sseqtrrd 3962 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ran 𝑔 ⊆ dom
𝐹) |
62 | | df-ss 3904 |
. . . . . . . . . . . . . 14
⊢ (ran
𝑔 ⊆ dom 𝐹 ↔ (ran 𝑔 ∩ dom 𝐹) = ran 𝑔) |
63 | 61, 62 | sylib 217 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (ran 𝑔 ∩ dom
𝐹) = ran 𝑔) |
64 | 58, 63 | eqtrid 2790 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (dom 𝐹 ∩ ran
𝑔) = ran 𝑔) |
65 | 13 | fdmd 6611 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ dom 𝑔 =
ω) |
66 | | peano1 7735 |
. . . . . . . . . . . . . . 15
⊢ ∅
∈ ω |
67 | | ne0i 4268 |
. . . . . . . . . . . . . . 15
⊢ (∅
∈ ω → ω ≠ ∅) |
68 | 66, 67 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ω ≠ ∅) |
69 | 65, 68 | eqnetrd 3011 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ dom 𝑔 ≠
∅) |
70 | | dm0rn0 5834 |
. . . . . . . . . . . . . 14
⊢ (dom
𝑔 = ∅ ↔ ran
𝑔 =
∅) |
71 | 70 | necon3bii 2996 |
. . . . . . . . . . . . 13
⊢ (dom
𝑔 ≠ ∅ ↔ ran
𝑔 ≠
∅) |
72 | 69, 71 | sylib 217 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ran 𝑔 ≠
∅) |
73 | 64, 72 | eqnetrd 3011 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (dom 𝐹 ∩ ran
𝑔) ≠
∅) |
74 | | imadisj 5988 |
. . . . . . . . . . . 12
⊢ ((𝐹 “ ran 𝑔) = ∅ ↔ (dom 𝐹 ∩ ran 𝑔) = ∅) |
75 | 74 | necon3bii 2996 |
. . . . . . . . . . 11
⊢ ((𝐹 “ ran 𝑔) ≠ ∅ ↔ (dom 𝐹 ∩ ran 𝑔) ≠ ∅) |
76 | 73, 75 | sylibr 233 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝐹 “ ran 𝑔) ≠ ∅) |
77 | 2 | isf34lem4 10133 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ ((𝐹 “ ran 𝑔) ⊆ 𝒫 𝐴 ∧ (𝐹 “ ran 𝑔) ≠ ∅)) → (𝐹‘∪ (𝐹 “ ran 𝑔)) = ∩ (𝐹 “ (𝐹 “ ran 𝑔))) |
78 | 10, 54, 76, 77 | syl12anc 834 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝐹‘∪ (𝐹
“ ran 𝑔)) = ∩ (𝐹
“ (𝐹 “ ran
𝑔))) |
79 | 2 | isf34lem3 10131 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ ran 𝑔 ⊆ 𝒫 𝐴) → (𝐹 “ (𝐹 “ ran 𝑔)) = ran 𝑔) |
80 | 10, 59, 79 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝐹 “ (𝐹 “ ran 𝑔)) = ran 𝑔) |
81 | 80 | inteqd 4884 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ∩ (𝐹 “ (𝐹 “ ran 𝑔)) = ∩ ran 𝑔) |
82 | 78, 81 | eqtrd 2778 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ (𝐹‘∪ (𝐹
“ ran 𝑔)) = ∩ ran 𝑔) |
83 | 82, 80 | eleq12d 2833 |
. . . . . . 7
⊢ (𝑔 ∈ (𝒫 𝐴 ↑m ω)
→ ((𝐹‘∪ (𝐹
“ ran 𝑔)) ∈
(𝐹 “ (𝐹 “ ran 𝑔)) ↔ ∩ ran
𝑔 ∈ ran 𝑔)) |
84 | 57, 83 | sylibd 238 |
. . . . . 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 3102 |
. . 3
⊢
(∀𝑓 ∈
(𝒫 𝐴
↑m ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓) → ∀𝑔 ∈ (𝒫 𝐴 ↑m
ω)(∀𝑦 ∈
ω (𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → ∩ ran
𝑔 ∈ ran 𝑔)) |
88 | | isfin3-3 10124 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔
∀𝑔 ∈ (𝒫
𝐴 ↑m
ω)(∀𝑦 ∈
ω (𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → ∩ ran
𝑔 ∈ ran 𝑔))) |
89 | 87, 88 | syl5ibr 245 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∀𝑓 ∈ (𝒫 𝐴 ↑m ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓) → 𝐴 ∈ FinIII)) |
90 | 6, 89 | impbid2 225 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔
∀𝑓 ∈ (𝒫
𝐴 ↑m
ω)(∀𝑦 ∈
ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓))) |