| Step | Hyp | Ref
| Expression |
| 1 | | isinf 9296 |
. 2
⊢ (¬
𝐴 ∈ Fin →
∀𝑛 ∈ ω
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)) |
| 2 | | omex 9683 |
. . 3
⊢ ω
∈ V |
| 3 | | sseq1 4009 |
. . . 4
⊢ (𝑥 = (𝑓‘𝑛) → (𝑥 ⊆ 𝐴 ↔ (𝑓‘𝑛) ⊆ 𝐴)) |
| 4 | | breq1 5146 |
. . . 4
⊢ (𝑥 = (𝑓‘𝑛) → (𝑥 ≈ 𝑛 ↔ (𝑓‘𝑛) ≈ 𝑛)) |
| 5 | 3, 4 | anbi12d 632 |
. . 3
⊢ (𝑥 = (𝑓‘𝑛) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛))) |
| 6 | 2, 5 | ac6s2 10526 |
. 2
⊢
(∀𝑛 ∈
ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) → ∃𝑓(𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛))) |
| 7 | | simpl 482 |
. . . . . 6
⊢ (((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛) → (𝑓‘𝑛) ⊆ 𝐴) |
| 8 | 7 | ralimi 3083 |
. . . . 5
⊢
(∀𝑛 ∈
ω ((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛) → ∀𝑛 ∈ ω (𝑓‘𝑛) ⊆ 𝐴) |
| 9 | | fvex 6919 |
. . . . . . . 8
⊢ (𝑓‘𝑛) ∈ V |
| 10 | 9 | elpw 4604 |
. . . . . . 7
⊢ ((𝑓‘𝑛) ∈ 𝒫 𝐴 ↔ (𝑓‘𝑛) ⊆ 𝐴) |
| 11 | 10 | ralbii 3093 |
. . . . . 6
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛) ∈ 𝒫 𝐴 ↔ ∀𝑛 ∈ ω (𝑓‘𝑛) ⊆ 𝐴) |
| 12 | | fnfvrnss 7141 |
. . . . . . 7
⊢ ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω (𝑓‘𝑛) ∈ 𝒫 𝐴) → ran 𝑓 ⊆ 𝒫 𝐴) |
| 13 | | uniss 4915 |
. . . . . . . 8
⊢ (ran
𝑓 ⊆ 𝒫 𝐴 → ∪ ran 𝑓 ⊆ ∪
𝒫 𝐴) |
| 14 | | unipw 5455 |
. . . . . . . 8
⊢ ∪ 𝒫 𝐴 = 𝐴 |
| 15 | 13, 14 | sseqtrdi 4024 |
. . . . . . 7
⊢ (ran
𝑓 ⊆ 𝒫 𝐴 → ∪ ran 𝑓 ⊆ 𝐴) |
| 16 | 12, 15 | syl 17 |
. . . . . 6
⊢ ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω (𝑓‘𝑛) ∈ 𝒫 𝐴) → ∪ ran
𝑓 ⊆ 𝐴) |
| 17 | 11, 16 | sylan2br 595 |
. . . . 5
⊢ ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω (𝑓‘𝑛) ⊆ 𝐴) → ∪ ran
𝑓 ⊆ 𝐴) |
| 18 | 8, 17 | sylan2 593 |
. . . 4
⊢ ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛)) → ∪ ran
𝑓 ⊆ 𝐴) |
| 19 | | dffn5 6967 |
. . . . . . . . . . 11
⊢ (𝑓 Fn ω ↔ 𝑓 = (𝑛 ∈ ω ↦ (𝑓‘𝑛))) |
| 20 | 19 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑓 Fn ω → 𝑓 = (𝑛 ∈ ω ↦ (𝑓‘𝑛))) |
| 21 | 20 | rneqd 5949 |
. . . . . . . . 9
⊢ (𝑓 Fn ω → ran 𝑓 = ran (𝑛 ∈ ω ↦ (𝑓‘𝑛))) |
| 22 | 21 | unieqd 4920 |
. . . . . . . 8
⊢ (𝑓 Fn ω → ∪ ran 𝑓 = ∪ ran (𝑛 ∈ ω ↦ (𝑓‘𝑛))) |
| 23 | 9 | dfiun3 5980 |
. . . . . . . 8
⊢ ∪ 𝑛 ∈ ω (𝑓‘𝑛) = ∪ ran (𝑛 ∈ ω ↦ (𝑓‘𝑛)) |
| 24 | 22, 23 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑓 Fn ω → ∪ ran 𝑓 = ∪ 𝑛 ∈ ω (𝑓‘𝑛)) |
| 25 | 24 | adantr 480 |
. . . . . 6
⊢ ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛)) → ∪ ran
𝑓 = ∪ 𝑛 ∈ ω (𝑓‘𝑛)) |
| 26 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛) → (𝑓‘𝑛) ≈ 𝑛) |
| 27 | 26 | ralimi 3083 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ω ((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛) → ∀𝑛 ∈ ω (𝑓‘𝑛) ≈ 𝑛) |
| 28 | | endom 9019 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑛) ≈ 𝑛 → (𝑓‘𝑛) ≼ 𝑛) |
| 29 | | nnsdom 9694 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ω → 𝑛 ≺
ω) |
| 30 | | domsdomtr 9152 |
. . . . . . . . . . 11
⊢ (((𝑓‘𝑛) ≼ 𝑛 ∧ 𝑛 ≺ ω) → (𝑓‘𝑛) ≺ ω) |
| 31 | | sdomdom 9020 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑛) ≺ ω → (𝑓‘𝑛) ≼ ω) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑓‘𝑛) ≼ 𝑛 ∧ 𝑛 ≺ ω) → (𝑓‘𝑛) ≼ ω) |
| 33 | 28, 29, 32 | syl2anr 597 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ω ∧ (𝑓‘𝑛) ≈ 𝑛) → (𝑓‘𝑛) ≼ ω) |
| 34 | 33 | ralimiaa 3082 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛) ≈ 𝑛 → ∀𝑛 ∈ ω (𝑓‘𝑛) ≼ ω) |
| 35 | | iunctb2 37404 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛) ≼ ω →
∪ 𝑛 ∈ ω (𝑓‘𝑛) ≼ ω) |
| 36 | 27, 34, 35 | 3syl 18 |
. . . . . . 7
⊢
(∀𝑛 ∈
ω ((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛) → ∪
𝑛 ∈ ω (𝑓‘𝑛) ≼ ω) |
| 37 | 36 | adantl 481 |
. . . . . 6
⊢ ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛)) → ∪
𝑛 ∈ ω (𝑓‘𝑛) ≼ ω) |
| 38 | 25, 37 | eqbrtrd 5165 |
. . . . 5
⊢ ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛)) → ∪ ran
𝑓 ≼
ω) |
| 39 | | fvssunirn 6939 |
. . . . . . . . . 10
⊢ (𝑓‘𝑛) ⊆ ∪ ran
𝑓 |
| 40 | 39 | jctl 523 |
. . . . . . . . 9
⊢ ((𝑓‘𝑛) ≈ 𝑛 → ((𝑓‘𝑛) ⊆ ∪ ran
𝑓 ∧ (𝑓‘𝑛) ≈ 𝑛)) |
| 41 | 40 | adantl 481 |
. . . . . . . 8
⊢ (((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛) → ((𝑓‘𝑛) ⊆ ∪ ran
𝑓 ∧ (𝑓‘𝑛) ≈ 𝑛)) |
| 42 | 41 | ralimi 3083 |
. . . . . . 7
⊢
(∀𝑛 ∈
ω ((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛) → ∀𝑛 ∈ ω ((𝑓‘𝑛) ⊆ ∪ ran
𝑓 ∧ (𝑓‘𝑛) ≈ 𝑛)) |
| 43 | | sseq1 4009 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑓‘𝑛) → (𝑥 ⊆ ∪ ran
𝑓 ↔ (𝑓‘𝑛) ⊆ ∪ ran
𝑓)) |
| 44 | 43, 4 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑓‘𝑛) → ((𝑥 ⊆ ∪ ran
𝑓 ∧ 𝑥 ≈ 𝑛) ↔ ((𝑓‘𝑛) ⊆ ∪ ran
𝑓 ∧ (𝑓‘𝑛) ≈ 𝑛))) |
| 45 | 9, 44 | spcev 3606 |
. . . . . . . . . 10
⊢ (((𝑓‘𝑛) ⊆ ∪ ran
𝑓 ∧ (𝑓‘𝑛) ≈ 𝑛) → ∃𝑥(𝑥 ⊆ ∪ ran
𝑓 ∧ 𝑥 ≈ 𝑛)) |
| 46 | 45 | ralimi 3083 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ω ((𝑓‘𝑛) ⊆ ∪ ran 𝑓 ∧ (𝑓‘𝑛) ≈ 𝑛) → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ ∪ ran
𝑓 ∧ 𝑥 ≈ 𝑛)) |
| 47 | | isinf2 37406 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ω ∃𝑥(𝑥 ⊆ ∪ ran 𝑓 ∧ 𝑥 ≈ 𝑛) → ¬ ∪
ran 𝑓 ∈
Fin) |
| 48 | 46, 47 | syl 17 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ω ((𝑓‘𝑛) ⊆ ∪ ran 𝑓 ∧ (𝑓‘𝑛) ≈ 𝑛) → ¬ ∪
ran 𝑓 ∈
Fin) |
| 49 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑓 ∈ V |
| 50 | 49 | rnex 7932 |
. . . . . . . . . 10
⊢ ran 𝑓 ∈ V |
| 51 | 50 | uniex 7761 |
. . . . . . . . 9
⊢ ∪ ran 𝑓 ∈ V |
| 52 | | infinf 10606 |
. . . . . . . . 9
⊢ (∪ ran 𝑓 ∈ V → (¬ ∪ ran 𝑓 ∈ Fin ↔ ω ≼ ∪ ran 𝑓)) |
| 53 | 51, 52 | ax-mp 5 |
. . . . . . . 8
⊢ (¬
∪ ran 𝑓 ∈ Fin ↔ ω ≼ ∪ ran 𝑓) |
| 54 | 48, 53 | sylib 218 |
. . . . . . 7
⊢
(∀𝑛 ∈
ω ((𝑓‘𝑛) ⊆ ∪ ran 𝑓 ∧ (𝑓‘𝑛) ≈ 𝑛) → ω ≼ ∪ ran 𝑓) |
| 55 | 42, 54 | syl 17 |
. . . . . 6
⊢
(∀𝑛 ∈
ω ((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛) → ω ≼ ∪ ran 𝑓) |
| 56 | 55 | adantl 481 |
. . . . 5
⊢ ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛)) → ω ≼ ∪ ran 𝑓) |
| 57 | | sbth 9133 |
. . . . 5
⊢ ((∪ ran 𝑓 ≼ ω ∧ ω ≼ ∪ ran 𝑓) → ∪ ran
𝑓 ≈
ω) |
| 58 | 38, 56, 57 | syl2anc 584 |
. . . 4
⊢ ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛)) → ∪ ran
𝑓 ≈
ω) |
| 59 | | sseq1 4009 |
. . . . . 6
⊢ (𝑥 = ∪
ran 𝑓 → (𝑥 ⊆ 𝐴 ↔ ∪ ran
𝑓 ⊆ 𝐴)) |
| 60 | | breq1 5146 |
. . . . . 6
⊢ (𝑥 = ∪
ran 𝑓 → (𝑥 ≈ ω ↔ ∪ ran 𝑓 ≈ ω)) |
| 61 | 59, 60 | anbi12d 632 |
. . . . 5
⊢ (𝑥 = ∪
ran 𝑓 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ω) ↔ (∪ ran 𝑓 ⊆ 𝐴 ∧ ∪ ran
𝑓 ≈
ω))) |
| 62 | 51, 61 | spcev 3606 |
. . . 4
⊢ ((∪ ran 𝑓 ⊆ 𝐴 ∧ ∪ ran
𝑓 ≈ ω) →
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ω)) |
| 63 | 18, 58, 62 | syl2anc 584 |
. . 3
⊢ ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛)) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ω)) |
| 64 | 63 | exlimiv 1930 |
. 2
⊢
(∃𝑓(𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓‘𝑛) ⊆ 𝐴 ∧ (𝑓‘𝑛) ≈ 𝑛)) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ω)) |
| 65 | 1, 6, 64 | 3syl 18 |
1
⊢ (¬
𝐴 ∈ Fin →
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ω)) |