Step | Hyp | Ref
| Expression |
1 | | elmapi 7765 |
. . . 4
⊢ (𝑓 ∈ (𝒫 𝐴 ↑𝑚
ω) → 𝑓:ω⟶𝒫 𝐴) |
2 | | compss.a |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) |
3 | 2 | isf34lem7 9084 |
. . . . 5
⊢ ((𝐴 ∈ FinIII ∧
𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦)) → ∪ ran
𝑓 ∈ ran 𝑓) |
4 | 3 | 3expia 1259 |
. . . 4
⊢ ((𝐴 ∈ FinIII ∧
𝑓:ω⟶𝒫
𝐴) → (∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓)) |
5 | 1, 4 | sylan2 490 |
. . 3
⊢ ((𝐴 ∈ FinIII ∧
𝑓 ∈ (𝒫 𝐴 ↑𝑚
ω)) → (∀𝑦
∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓)) |
6 | 5 | ralrimiva 2949 |
. 2
⊢ (𝐴 ∈ FinIII →
∀𝑓 ∈ (𝒫
𝐴
↑𝑚 ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓)) |
7 | | elmapex 7764 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → (𝒫 𝐴 ∈ V ∧ ω ∈
V)) |
8 | 7 | simpld 474 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → 𝒫 𝐴
∈ V) |
9 | | pwexb 6867 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V) |
10 | 8, 9 | sylibr 223 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → 𝐴 ∈
V) |
11 | 2 | isf34lem2 9078 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → 𝐹:𝒫 𝐴⟶𝒫 𝐴) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → 𝐹:𝒫
𝐴⟶𝒫 𝐴) |
13 | | elmapi 7765 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → 𝑔:ω⟶𝒫 𝐴) |
14 | | fco 5971 |
. . . . . . . 8
⊢ ((𝐹:𝒫 𝐴⟶𝒫 𝐴 ∧ 𝑔:ω⟶𝒫 𝐴) → (𝐹 ∘ 𝑔):ω⟶𝒫 𝐴) |
15 | 12, 13, 14 | syl2anc 691 |
. . . . . . 7
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → (𝐹 ∘
𝑔):ω⟶𝒫
𝐴) |
16 | | elmapg 7757 |
. . . . . . . 8
⊢
((𝒫 𝐴 ∈
V ∧ ω ∈ V) → ((𝐹 ∘ 𝑔) ∈ (𝒫 𝐴 ↑𝑚 ω) ↔
(𝐹 ∘ 𝑔):ω⟶𝒫 𝐴)) |
17 | 7, 16 | syl 17 |
. . . . . . 7
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → ((𝐹 ∘
𝑔) ∈ (𝒫 𝐴 ↑𝑚
ω) ↔ (𝐹 ∘
𝑔):ω⟶𝒫
𝐴)) |
18 | 15, 17 | mpbird 246 |
. . . . . 6
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → (𝐹 ∘
𝑔) ∈ (𝒫 𝐴 ↑𝑚
ω)) |
19 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑓 = (𝐹 ∘ 𝑔) → (𝑓‘𝑦) = ((𝐹 ∘ 𝑔)‘𝑦)) |
20 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑓 = (𝐹 ∘ 𝑔) → (𝑓‘suc 𝑦) = ((𝐹 ∘ 𝑔)‘suc 𝑦)) |
21 | 19, 20 | sseq12d 3597 |
. . . . . . . . 9
⊢ (𝑓 = (𝐹 ∘ 𝑔) → ((𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) ↔ ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦))) |
22 | 21 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑓 = (𝐹 ∘ 𝑔) → (∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) ↔ ∀𝑦 ∈ ω ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦))) |
23 | | rneq 5272 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝐹 ∘ 𝑔) → ran 𝑓 = ran (𝐹 ∘ 𝑔)) |
24 | | rnco2 5559 |
. . . . . . . . . . 11
⊢ ran
(𝐹 ∘ 𝑔) = (𝐹 “ ran 𝑔) |
25 | 23, 24 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝑓 = (𝐹 ∘ 𝑔) → ran 𝑓 = (𝐹 “ ran 𝑔)) |
26 | 25 | unieqd 4382 |
. . . . . . . . 9
⊢ (𝑓 = (𝐹 ∘ 𝑔) → ∪ ran
𝑓 = ∪ (𝐹
“ ran 𝑔)) |
27 | 26, 25 | eleq12d 2682 |
. . . . . . . 8
⊢ (𝑓 = (𝐹 ∘ 𝑔) → (∪ ran
𝑓 ∈ ran 𝑓 ↔ ∪ (𝐹
“ ran 𝑔) ∈
(𝐹 “ ran 𝑔))) |
28 | 22, 27 | imbi12d 333 |
. . . . . . 7
⊢ (𝑓 = (𝐹 ∘ 𝑔) → ((∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓) ↔ (∀𝑦 ∈ ω ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦) → ∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔)))) |
29 | 28 | rspccv 3279 |
. . . . . 6
⊢
(∀𝑓 ∈
(𝒫 𝐴
↑𝑚 ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓) → ((𝐹 ∘ 𝑔) ∈ (𝒫 𝐴 ↑𝑚 ω) →
(∀𝑦 ∈ ω
((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦) → ∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔)))) |
30 | 18, 29 | syl5 33 |
. . . . 5
⊢
(∀𝑓 ∈
(𝒫 𝐴
↑𝑚 ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓) → (𝑔 ∈ (𝒫 𝐴 ↑𝑚 ω) →
(∀𝑦 ∈ ω
((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦) → ∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔)))) |
31 | | sscon 3706 |
. . . . . . . . 9
⊢ ((𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → (𝐴 ∖ (𝑔‘𝑦)) ⊆ (𝐴 ∖ (𝑔‘suc 𝑦))) |
32 | 10 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) ∧ 𝑦 ∈
ω) → 𝐴 ∈
V) |
33 | 13 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) ∧ 𝑦 ∈
ω) → (𝑔‘𝑦) ∈ 𝒫 𝐴) |
34 | 33 | elpwid 4118 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) ∧ 𝑦 ∈
ω) → (𝑔‘𝑦) ⊆ 𝐴) |
35 | 2 | isf34lem1 9077 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (𝑔‘𝑦) ⊆ 𝐴) → (𝐹‘(𝑔‘𝑦)) = (𝐴 ∖ (𝑔‘𝑦))) |
36 | 32, 34, 35 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) ∧ 𝑦 ∈
ω) → (𝐹‘(𝑔‘𝑦)) = (𝐴 ∖ (𝑔‘𝑦))) |
37 | | peano2 6978 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ω → suc 𝑦 ∈
ω) |
38 | | ffvelrn 6265 |
. . . . . . . . . . . . 13
⊢ ((𝑔:ω⟶𝒫 𝐴 ∧ suc 𝑦 ∈ ω) → (𝑔‘suc 𝑦) ∈ 𝒫 𝐴) |
39 | 13, 37, 38 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) ∧ 𝑦 ∈
ω) → (𝑔‘suc 𝑦) ∈ 𝒫 𝐴) |
40 | 39 | elpwid 4118 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) ∧ 𝑦 ∈
ω) → (𝑔‘suc 𝑦) ⊆ 𝐴) |
41 | 2 | isf34lem1 9077 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (𝑔‘suc 𝑦) ⊆ 𝐴) → (𝐹‘(𝑔‘suc 𝑦)) = (𝐴 ∖ (𝑔‘suc 𝑦))) |
42 | 32, 40, 41 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) ∧ 𝑦 ∈
ω) → (𝐹‘(𝑔‘suc 𝑦)) = (𝐴 ∖ (𝑔‘suc 𝑦))) |
43 | 36, 42 | sseq12d 3597 |
. . . . . . . . 9
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) ∧ 𝑦 ∈
ω) → ((𝐹‘(𝑔‘𝑦)) ⊆ (𝐹‘(𝑔‘suc 𝑦)) ↔ (𝐴 ∖ (𝑔‘𝑦)) ⊆ (𝐴 ∖ (𝑔‘suc 𝑦)))) |
44 | 31, 43 | syl5ibr 235 |
. . . . . . . 8
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) ∧ 𝑦 ∈
ω) → ((𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → (𝐹‘(𝑔‘𝑦)) ⊆ (𝐹‘(𝑔‘suc 𝑦)))) |
45 | | fvco3 6185 |
. . . . . . . . . 10
⊢ ((𝑔:ω⟶𝒫 𝐴 ∧ 𝑦 ∈ ω) → ((𝐹 ∘ 𝑔)‘𝑦) = (𝐹‘(𝑔‘𝑦))) |
46 | 13, 45 | sylan 487 |
. . . . . . . . 9
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) ∧ 𝑦 ∈
ω) → ((𝐹 ∘
𝑔)‘𝑦) = (𝐹‘(𝑔‘𝑦))) |
47 | | fvco3 6185 |
. . . . . . . . . 10
⊢ ((𝑔:ω⟶𝒫 𝐴 ∧ suc 𝑦 ∈ ω) → ((𝐹 ∘ 𝑔)‘suc 𝑦) = (𝐹‘(𝑔‘suc 𝑦))) |
48 | 13, 37, 47 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) ∧ 𝑦 ∈
ω) → ((𝐹 ∘
𝑔)‘suc 𝑦) = (𝐹‘(𝑔‘suc 𝑦))) |
49 | 46, 48 | sseq12d 3597 |
. . . . . . . 8
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) ∧ 𝑦 ∈
ω) → (((𝐹
∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦) ↔ (𝐹‘(𝑔‘𝑦)) ⊆ (𝐹‘(𝑔‘suc 𝑦)))) |
50 | 44, 49 | sylibrd 248 |
. . . . . . 7
⊢ ((𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) ∧ 𝑦 ∈
ω) → ((𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦))) |
51 | 50 | ralimdva 2945 |
. . . . . 6
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → (∀𝑦
∈ ω (𝑔‘suc
𝑦) ⊆ (𝑔‘𝑦) → ∀𝑦 ∈ ω ((𝐹 ∘ 𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦))) |
52 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐹:𝒫 𝐴⟶𝒫 𝐴 → 𝐹 Fn 𝒫 𝐴) |
53 | 12, 52 | syl 17 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → 𝐹 Fn
𝒫 𝐴) |
54 | | imassrn 5396 |
. . . . . . . . 9
⊢ (𝐹 “ ran 𝑔) ⊆ ran 𝐹 |
55 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝐹:𝒫 𝐴⟶𝒫 𝐴 → ran 𝐹 ⊆ 𝒫 𝐴) |
56 | 12, 55 | syl 17 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → ran 𝐹
⊆ 𝒫 𝐴) |
57 | 54, 56 | syl5ss 3579 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → (𝐹 “
ran 𝑔) ⊆ 𝒫
𝐴) |
58 | | fnfvima 6400 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝒫 𝐴 ∧ (𝐹 “ ran 𝑔) ⊆ 𝒫 𝐴 ∧ ∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔)) → (𝐹‘∪ (𝐹 “ ran 𝑔)) ∈ (𝐹 “ (𝐹 “ ran 𝑔))) |
59 | 58 | 3expia 1259 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝒫 𝐴 ∧ (𝐹 “ ran 𝑔) ⊆ 𝒫 𝐴) → (∪
(𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔) → (𝐹‘∪ (𝐹 “ ran 𝑔)) ∈ (𝐹 “ (𝐹 “ ran 𝑔)))) |
60 | 53, 57, 59 | syl2anc 691 |
. . . . . . 7
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → (∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔) → (𝐹‘∪ (𝐹 “ ran 𝑔)) ∈ (𝐹 “ (𝐹 “ ran 𝑔)))) |
61 | | incom 3767 |
. . . . . . . . . . . . 13
⊢ (dom
𝐹 ∩ ran 𝑔) = (ran 𝑔 ∩ dom 𝐹) |
62 | | frn 5966 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:ω⟶𝒫 𝐴 → ran 𝑔 ⊆ 𝒫 𝐴) |
63 | 13, 62 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → ran 𝑔
⊆ 𝒫 𝐴) |
64 | | fdm 5964 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝒫 𝐴⟶𝒫 𝐴 → dom 𝐹 = 𝒫 𝐴) |
65 | 12, 64 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → dom 𝐹 =
𝒫 𝐴) |
66 | 63, 65 | sseqtr4d 3605 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → ran 𝑔
⊆ dom 𝐹) |
67 | | df-ss 3554 |
. . . . . . . . . . . . . 14
⊢ (ran
𝑔 ⊆ dom 𝐹 ↔ (ran 𝑔 ∩ dom 𝐹) = ran 𝑔) |
68 | 66, 67 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → (ran 𝑔
∩ dom 𝐹) = ran 𝑔) |
69 | 61, 68 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → (dom 𝐹
∩ ran 𝑔) = ran 𝑔) |
70 | | fdm 5964 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:ω⟶𝒫 𝐴 → dom 𝑔 = ω) |
71 | 13, 70 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → dom 𝑔 =
ω) |
72 | | peano1 6977 |
. . . . . . . . . . . . . . 15
⊢ ∅
∈ ω |
73 | | ne0i 3880 |
. . . . . . . . . . . . . . 15
⊢ (∅
∈ ω → ω ≠ ∅) |
74 | 72, 73 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → ω ≠ ∅) |
75 | 71, 74 | eqnetrd 2849 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → dom 𝑔 ≠
∅) |
76 | | dm0rn0 5263 |
. . . . . . . . . . . . . 14
⊢ (dom
𝑔 = ∅ ↔ ran
𝑔 =
∅) |
77 | 76 | necon3bii 2834 |
. . . . . . . . . . . . 13
⊢ (dom
𝑔 ≠ ∅ ↔ ran
𝑔 ≠
∅) |
78 | 75, 77 | sylib 207 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → ran 𝑔 ≠
∅) |
79 | 69, 78 | eqnetrd 2849 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → (dom 𝐹
∩ ran 𝑔) ≠
∅) |
80 | | imadisj 5403 |
. . . . . . . . . . . 12
⊢ ((𝐹 “ ran 𝑔) = ∅ ↔ (dom 𝐹 ∩ ran 𝑔) = ∅) |
81 | 80 | necon3bii 2834 |
. . . . . . . . . . 11
⊢ ((𝐹 “ ran 𝑔) ≠ ∅ ↔ (dom 𝐹 ∩ ran 𝑔) ≠ ∅) |
82 | 79, 81 | sylibr 223 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → (𝐹 “
ran 𝑔) ≠
∅) |
83 | 2 | isf34lem4 9082 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ ((𝐹 “ ran 𝑔) ⊆ 𝒫 𝐴 ∧ (𝐹 “ ran 𝑔) ≠ ∅)) → (𝐹‘∪ (𝐹 “ ran 𝑔)) = ∩ (𝐹 “ (𝐹 “ ran 𝑔))) |
84 | 10, 57, 82, 83 | syl12anc 1316 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → (𝐹‘∪ (𝐹 “ ran 𝑔)) = ∩ (𝐹 “ (𝐹 “ ran 𝑔))) |
85 | 2 | isf34lem3 9080 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ ran 𝑔 ⊆ 𝒫 𝐴) → (𝐹 “ (𝐹 “ ran 𝑔)) = ran 𝑔) |
86 | 10, 63, 85 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → (𝐹 “
(𝐹 “ ran 𝑔)) = ran 𝑔) |
87 | 86 | inteqd 4415 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → ∩ (𝐹 “ (𝐹 “ ran 𝑔)) = ∩ ran 𝑔) |
88 | 84, 87 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → (𝐹‘∪ (𝐹 “ ran 𝑔)) = ∩ ran 𝑔) |
89 | 88, 86 | eleq12d 2682 |
. . . . . . 7
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → ((𝐹‘∪ (𝐹 “ ran 𝑔)) ∈ (𝐹 “ (𝐹 “ ran 𝑔)) ↔ ∩ ran
𝑔 ∈ ran 𝑔)) |
90 | 60, 89 | sylibd 228 |
. . . . . 6
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → (∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔) → ∩ ran
𝑔 ∈ ran 𝑔)) |
91 | 51, 90 | imim12d 79 |
. . . . 5
⊢ (𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω) → ((∀𝑦
∈ ω ((𝐹 ∘
𝑔)‘𝑦) ⊆ ((𝐹 ∘ 𝑔)‘suc 𝑦) → ∪ (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔)) → (∀𝑦 ∈ ω (𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → ∩ ran
𝑔 ∈ ran 𝑔))) |
92 | 30, 91 | sylcom 30 |
. . . 4
⊢
(∀𝑓 ∈
(𝒫 𝐴
↑𝑚 ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓) → (𝑔 ∈ (𝒫 𝐴 ↑𝑚 ω) →
(∀𝑦 ∈ ω
(𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → ∩ ran
𝑔 ∈ ran 𝑔))) |
93 | 92 | ralrimiv 2948 |
. . 3
⊢
(∀𝑓 ∈
(𝒫 𝐴
↑𝑚 ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓) → ∀𝑔 ∈ (𝒫 𝐴 ↑𝑚
ω)(∀𝑦 ∈
ω (𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → ∩ ran
𝑔 ∈ ran 𝑔)) |
94 | | isfin3-3 9073 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔
∀𝑔 ∈ (𝒫
𝐴
↑𝑚 ω)(∀𝑦 ∈ ω (𝑔‘suc 𝑦) ⊆ (𝑔‘𝑦) → ∩ ran
𝑔 ∈ ran 𝑔))) |
95 | 93, 94 | syl5ibr 235 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∀𝑓 ∈ (𝒫 𝐴 ↑𝑚
ω)(∀𝑦 ∈
ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓) → 𝐴 ∈ FinIII)) |
96 | 6, 95 | impbid2 215 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔
∀𝑓 ∈ (𝒫
𝐴
↑𝑚 ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran
𝑓 ∈ ran 𝑓))) |