| Step | Hyp | Ref
| Expression |
| 1 | | brdomi 8999 |
. . . . 5
⊢ (ω
≼ 𝒫 𝐴 →
∃𝑏 𝑏:ω–1-1→𝒫 𝐴) |
| 2 | | fin23lem40.f |
. . . . . . . . . 10
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran
𝑎 ∈ ran 𝑎)} |
| 3 | 2 | fin23lem33 10385 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝐹 → ∃𝑐∀𝑑((𝑑:ω–1-1→V ∧ ∪ ran 𝑑 ⊆ 𝐴) → ((𝑐‘𝑑):ω–1-1→V ∧ ∪ ran (𝑐‘𝑑) ⊊ ∪ ran
𝑑))) |
| 4 | 3 | adantl 481 |
. . . . . . . 8
⊢ ((𝑏:ω–1-1→𝒫 𝐴 ∧ 𝐴 ∈ 𝐹) → ∃𝑐∀𝑑((𝑑:ω–1-1→V ∧ ∪ ran 𝑑 ⊆ 𝐴) → ((𝑐‘𝑑):ω–1-1→V ∧ ∪ ran (𝑐‘𝑑) ⊊ ∪ ran
𝑑))) |
| 5 | | ssv 4008 |
. . . . . . . . . . 11
⊢ 𝒫
𝐴 ⊆
V |
| 6 | | f1ss 6809 |
. . . . . . . . . . 11
⊢ ((𝑏:ω–1-1→𝒫 𝐴 ∧ 𝒫 𝐴 ⊆ V) → 𝑏:ω–1-1→V) |
| 7 | 5, 6 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑏:ω–1-1→𝒫 𝐴 → 𝑏:ω–1-1→V) |
| 8 | 7 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑏:ω–1-1→𝒫 𝐴 ∧ 𝐴 ∈ 𝐹) ∧ ∀𝑑((𝑑:ω–1-1→V ∧ ∪ ran 𝑑 ⊆ 𝐴) → ((𝑐‘𝑑):ω–1-1→V ∧ ∪ ran (𝑐‘𝑑) ⊊ ∪ ran
𝑑))) → 𝑏:ω–1-1→V) |
| 9 | | f1f 6804 |
. . . . . . . . . . . 12
⊢ (𝑏:ω–1-1→𝒫 𝐴 → 𝑏:ω⟶𝒫 𝐴) |
| 10 | | frn 6743 |
. . . . . . . . . . . 12
⊢ (𝑏:ω⟶𝒫 𝐴 → ran 𝑏 ⊆ 𝒫 𝐴) |
| 11 | | uniss 4915 |
. . . . . . . . . . . 12
⊢ (ran
𝑏 ⊆ 𝒫 𝐴 → ∪ ran 𝑏 ⊆ ∪
𝒫 𝐴) |
| 12 | 9, 10, 11 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑏:ω–1-1→𝒫 𝐴 → ∪ ran
𝑏 ⊆ ∪ 𝒫 𝐴) |
| 13 | | unipw 5455 |
. . . . . . . . . . 11
⊢ ∪ 𝒫 𝐴 = 𝐴 |
| 14 | 12, 13 | sseqtrdi 4024 |
. . . . . . . . . 10
⊢ (𝑏:ω–1-1→𝒫 𝐴 → ∪ ran
𝑏 ⊆ 𝐴) |
| 15 | 14 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑏:ω–1-1→𝒫 𝐴 ∧ 𝐴 ∈ 𝐹) ∧ ∀𝑑((𝑑:ω–1-1→V ∧ ∪ ran 𝑑 ⊆ 𝐴) → ((𝑐‘𝑑):ω–1-1→V ∧ ∪ ran (𝑐‘𝑑) ⊊ ∪ ran
𝑑))) → ∪ ran 𝑏 ⊆ 𝐴) |
| 16 | | f1eq1 6799 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 𝑒 → (𝑑:ω–1-1→V ↔ 𝑒:ω–1-1→V)) |
| 17 | | rneq 5947 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 𝑒 → ran 𝑑 = ran 𝑒) |
| 18 | 17 | unieqd 4920 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 𝑒 → ∪ ran
𝑑 = ∪ ran 𝑒) |
| 19 | 18 | sseq1d 4015 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 𝑒 → (∪ ran
𝑑 ⊆ 𝐴 ↔ ∪ ran
𝑒 ⊆ 𝐴)) |
| 20 | 16, 19 | anbi12d 632 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑒 → ((𝑑:ω–1-1→V ∧ ∪ ran 𝑑 ⊆ 𝐴) ↔ (𝑒:ω–1-1→V ∧ ∪ ran 𝑒 ⊆ 𝐴))) |
| 21 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 𝑒 → (𝑐‘𝑑) = (𝑐‘𝑒)) |
| 22 | | f1eq1 6799 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐‘𝑑) = (𝑐‘𝑒) → ((𝑐‘𝑑):ω–1-1→V ↔ (𝑐‘𝑒):ω–1-1→V)) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 𝑒 → ((𝑐‘𝑑):ω–1-1→V ↔ (𝑐‘𝑒):ω–1-1→V)) |
| 24 | 21 | rneqd 5949 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 𝑒 → ran (𝑐‘𝑑) = ran (𝑐‘𝑒)) |
| 25 | 24 | unieqd 4920 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 𝑒 → ∪ ran
(𝑐‘𝑑) = ∪ ran (𝑐‘𝑒)) |
| 26 | 25, 18 | psseq12d 4097 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 𝑒 → (∪ ran
(𝑐‘𝑑) ⊊ ∪ ran
𝑑 ↔ ∪ ran (𝑐‘𝑒) ⊊ ∪ ran
𝑒)) |
| 27 | 23, 26 | anbi12d 632 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑒 → (((𝑐‘𝑑):ω–1-1→V ∧ ∪ ran (𝑐‘𝑑) ⊊ ∪ ran
𝑑) ↔ ((𝑐‘𝑒):ω–1-1→V ∧ ∪ ran (𝑐‘𝑒) ⊊ ∪ ran
𝑒))) |
| 28 | 20, 27 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑒 → (((𝑑:ω–1-1→V ∧ ∪ ran 𝑑 ⊆ 𝐴) → ((𝑐‘𝑑):ω–1-1→V ∧ ∪ ran (𝑐‘𝑑) ⊊ ∪ ran
𝑑)) ↔ ((𝑒:ω–1-1→V ∧ ∪ ran 𝑒 ⊆ 𝐴) → ((𝑐‘𝑒):ω–1-1→V ∧ ∪ ran (𝑐‘𝑒) ⊊ ∪ ran
𝑒)))) |
| 29 | 28 | cbvalvw 2035 |
. . . . . . . . . . 11
⊢
(∀𝑑((𝑑:ω–1-1→V ∧ ∪ ran 𝑑 ⊆ 𝐴) → ((𝑐‘𝑑):ω–1-1→V ∧ ∪ ran (𝑐‘𝑑) ⊊ ∪ ran
𝑑)) ↔ ∀𝑒((𝑒:ω–1-1→V ∧ ∪ ran 𝑒 ⊆ 𝐴) → ((𝑐‘𝑒):ω–1-1→V ∧ ∪ ran (𝑐‘𝑒) ⊊ ∪ ran
𝑒))) |
| 30 | 29 | biimpi 216 |
. . . . . . . . . 10
⊢
(∀𝑑((𝑑:ω–1-1→V ∧ ∪ ran 𝑑 ⊆ 𝐴) → ((𝑐‘𝑑):ω–1-1→V ∧ ∪ ran (𝑐‘𝑑) ⊊ ∪ ran
𝑑)) → ∀𝑒((𝑒:ω–1-1→V ∧ ∪ ran 𝑒 ⊆ 𝐴) → ((𝑐‘𝑒):ω–1-1→V ∧ ∪ ran (𝑐‘𝑒) ⊊ ∪ ran
𝑒))) |
| 31 | 30 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑏:ω–1-1→𝒫 𝐴 ∧ 𝐴 ∈ 𝐹) ∧ ∀𝑑((𝑑:ω–1-1→V ∧ ∪ ran 𝑑 ⊆ 𝐴) → ((𝑐‘𝑑):ω–1-1→V ∧ ∪ ran (𝑐‘𝑑) ⊊ ∪ ran
𝑑))) → ∀𝑒((𝑒:ω–1-1→V ∧ ∪ ran 𝑒 ⊆ 𝐴) → ((𝑐‘𝑒):ω–1-1→V ∧ ∪ ran (𝑐‘𝑒) ⊊ ∪ ran
𝑒))) |
| 32 | | eqid 2737 |
. . . . . . . . 9
⊢
(rec(𝑐, 𝑏) ↾ ω) = (rec(𝑐, 𝑏) ↾ ω) |
| 33 | 2, 8, 15, 31, 32 | fin23lem39 10390 |
. . . . . . . 8
⊢ (((𝑏:ω–1-1→𝒫 𝐴 ∧ 𝐴 ∈ 𝐹) ∧ ∀𝑑((𝑑:ω–1-1→V ∧ ∪ ran 𝑑 ⊆ 𝐴) → ((𝑐‘𝑑):ω–1-1→V ∧ ∪ ran (𝑐‘𝑑) ⊊ ∪ ran
𝑑))) → ¬ 𝐴 ∈ 𝐹) |
| 34 | 4, 33 | exlimddv 1935 |
. . . . . . 7
⊢ ((𝑏:ω–1-1→𝒫 𝐴 ∧ 𝐴 ∈ 𝐹) → ¬ 𝐴 ∈ 𝐹) |
| 35 | 34 | pm2.01da 799 |
. . . . . 6
⊢ (𝑏:ω–1-1→𝒫 𝐴 → ¬ 𝐴 ∈ 𝐹) |
| 36 | 35 | exlimiv 1930 |
. . . . 5
⊢
(∃𝑏 𝑏:ω–1-1→𝒫 𝐴 → ¬ 𝐴 ∈ 𝐹) |
| 37 | 1, 36 | syl 17 |
. . . 4
⊢ (ω
≼ 𝒫 𝐴 →
¬ 𝐴 ∈ 𝐹) |
| 38 | 37 | con2i 139 |
. . 3
⊢ (𝐴 ∈ 𝐹 → ¬ ω ≼ 𝒫
𝐴) |
| 39 | | pwexg 5378 |
. . . 4
⊢ (𝐴 ∈ 𝐹 → 𝒫 𝐴 ∈ V) |
| 40 | | isfin4-2 10354 |
. . . 4
⊢
(𝒫 𝐴 ∈
V → (𝒫 𝐴
∈ FinIV ↔ ¬ ω ≼ 𝒫 𝐴)) |
| 41 | 39, 40 | syl 17 |
. . 3
⊢ (𝐴 ∈ 𝐹 → (𝒫 𝐴 ∈ FinIV ↔ ¬
ω ≼ 𝒫 𝐴)) |
| 42 | 38, 41 | mpbird 257 |
. 2
⊢ (𝐴 ∈ 𝐹 → 𝒫 𝐴 ∈ FinIV) |
| 43 | | isfin3 10336 |
. 2
⊢ (𝐴 ∈ FinIII ↔
𝒫 𝐴 ∈
FinIV) |
| 44 | 42, 43 | sylibr 234 |
1
⊢ (𝐴 ∈ 𝐹 → 𝐴 ∈ FinIII) |