| Step | Hyp | Ref
| Expression |
| 1 | | breq2 5147 |
. . . . . 6
⊢ (𝑛 = ∅ → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ ∅)) |
| 2 | 1 | anbi2d 630 |
. . . . 5
⊢ (𝑛 = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅))) |
| 3 | 2 | exbidv 1921 |
. . . 4
⊢ (𝑛 = ∅ → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅))) |
| 4 | | breq2 5147 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑚)) |
| 5 | 4 | anbi2d 630 |
. . . . 5
⊢ (𝑛 = 𝑚 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚))) |
| 6 | 5 | exbidv 1921 |
. . . 4
⊢ (𝑛 = 𝑚 → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚))) |
| 7 | | sseq1 4009 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
| 8 | 7 | adantl 481 |
. . . . . 6
⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
| 9 | | breq1 5146 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑛 ↔ 𝑦 ≈ 𝑛)) |
| 10 | | breq2 5147 |
. . . . . . 7
⊢ (𝑛 = suc 𝑚 → (𝑦 ≈ 𝑛 ↔ 𝑦 ≈ suc 𝑚)) |
| 11 | 9, 10 | sylan9bbr 510 |
. . . . . 6
⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → (𝑥 ≈ 𝑛 ↔ 𝑦 ≈ suc 𝑚)) |
| 12 | 8, 11 | anbi12d 632 |
. . . . 5
⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))) |
| 13 | 12 | cbvexdvaw 2038 |
. . . 4
⊢ (𝑛 = suc 𝑚 → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))) |
| 14 | | 0ss 4400 |
. . . . . 6
⊢ ∅
⊆ 𝐴 |
| 15 | | peano1 7910 |
. . . . . . 7
⊢ ∅
∈ ω |
| 16 | | enrefnn 9087 |
. . . . . . 7
⊢ (∅
∈ ω → ∅ ≈ ∅) |
| 17 | 15, 16 | ax-mp 5 |
. . . . . 6
⊢ ∅
≈ ∅ |
| 18 | | 0ex 5307 |
. . . . . . 7
⊢ ∅
∈ V |
| 19 | | sseq1 4009 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
| 20 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑥 ≈ ∅ ↔ ∅
≈ ∅)) |
| 21 | 19, 20 | anbi12d 632 |
. . . . . . 7
⊢ (𝑥 = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅) ↔ (∅ ⊆
𝐴 ∧ ∅ ≈
∅))) |
| 22 | 18, 21 | spcev 3606 |
. . . . . 6
⊢ ((∅
⊆ 𝐴 ∧ ∅
≈ ∅) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅)) |
| 23 | 14, 17, 22 | mp2an 692 |
. . . . 5
⊢
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅) |
| 24 | 23 | a1i 11 |
. . . 4
⊢ (¬
𝐴 ∈ Fin →
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅)) |
| 25 | | ssdif0 4366 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ 𝑥 ↔ (𝐴 ∖ 𝑥) = ∅) |
| 26 | | eqss 3999 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐴 ↔ (𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥)) |
| 27 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝐴 → (𝑥 ≈ 𝑚 ↔ 𝐴 ≈ 𝑚)) |
| 28 | 27 | biimpa 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚) → 𝐴 ≈ 𝑚) |
| 29 | | rspe 3249 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ∈ ω ∧ 𝐴 ≈ 𝑚) → ∃𝑚 ∈ ω 𝐴 ≈ 𝑚) |
| 30 | 28, 29 | sylan2 593 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ω ∧ (𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚)) → ∃𝑚 ∈ ω 𝐴 ≈ 𝑚) |
| 31 | | isfi 9016 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ Fin ↔ ∃𝑚 ∈ ω 𝐴 ≈ 𝑚) |
| 32 | 30, 31 | sylibr 234 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ω ∧ (𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚)) → 𝐴 ∈ Fin) |
| 33 | 32 | expcom 413 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin)) |
| 34 | 26, 33 | sylanbr 582 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥) ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin)) |
| 35 | 34 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥) → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin))) |
| 36 | 25, 35 | sylan2br 595 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ 𝐴 ∧ (𝐴 ∖ 𝑥) = ∅) → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin))) |
| 37 | 36 | expcom 413 |
. . . . . . . . . . 11
⊢ ((𝐴 ∖ 𝑥) = ∅ → (𝑥 ⊆ 𝐴 → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin)))) |
| 38 | 37 | 3impd 1349 |
. . . . . . . . . 10
⊢ ((𝐴 ∖ 𝑥) = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → 𝐴 ∈ Fin)) |
| 39 | 38 | com12 32 |
. . . . . . . . 9
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → ((𝐴 ∖ 𝑥) = ∅ → 𝐴 ∈ Fin)) |
| 40 | 39 | con3d 152 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ¬ (𝐴 ∖ 𝑥) = ∅)) |
| 41 | | bren 8995 |
. . . . . . . . . 10
⊢ (𝑥 ≈ 𝑚 ↔ ∃𝑓 𝑓:𝑥–1-1-onto→𝑚) |
| 42 | | neq0 4352 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝐴 ∖ 𝑥) = ∅ ↔ ∃𝑧 𝑧 ∈ (𝐴 ∖ 𝑥)) |
| 43 | | eldifi 4131 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → 𝑧 ∈ 𝐴) |
| 44 | 43 | snssd 4809 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → {𝑧} ⊆ 𝐴) |
| 45 | | unss 4190 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴) ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴) |
| 46 | 45 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴) → (𝑥 ∪ {𝑧}) ⊆ 𝐴) |
| 47 | 44, 46 | sylan2 593 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑥)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴) |
| 48 | 47 | ad2ant2r 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴) |
| 49 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑧 ∈ V |
| 50 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑚 ∈ V |
| 51 | 49, 50 | f1osn 6888 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
{〈𝑧, 𝑚〉}:{𝑧}–1-1-onto→{𝑚} |
| 52 | 51 | jctr 524 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓:𝑥–1-1-onto→𝑚 → (𝑓:𝑥–1-1-onto→𝑚 ∧ {〈𝑧, 𝑚〉}:{𝑧}–1-1-onto→{𝑚})) |
| 53 | | eldifn 4132 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → ¬ 𝑧 ∈ 𝑥) |
| 54 | | disjsn 4711 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑥) |
| 55 | 53, 54 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑥 ∩ {𝑧}) = ∅) |
| 56 | | nnord 7895 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ω → Ord 𝑚) |
| 57 | | orddisj 6422 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Ord
𝑚 → (𝑚 ∩ {𝑚}) = ∅) |
| 58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ω → (𝑚 ∩ {𝑚}) = ∅) |
| 59 | 55, 58 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω) → ((𝑥 ∩ {𝑧}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅)) |
| 60 | | f1oun 6867 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑓:𝑥–1-1-onto→𝑚 ∧ {〈𝑧, 𝑚〉}:{𝑧}–1-1-onto→{𝑚}) ∧ ((𝑥 ∩ {𝑧}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅)) → (𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚})) |
| 61 | 52, 59, 60 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓:𝑥–1-1-onto→𝑚 ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚})) |
| 62 | | df-suc 6390 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ suc 𝑚 = (𝑚 ∪ {𝑚}) |
| 63 | | f1oeq3 6838 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (suc
𝑚 = (𝑚 ∪ {𝑚}) → ((𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚 ↔ (𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))) |
| 64 | 62, 63 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚 ↔ (𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚})) |
| 65 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑓 ∈ V |
| 66 | | snex 5436 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
{〈𝑧, 𝑚〉} ∈
V |
| 67 | 65, 66 | unex 7764 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∪ {〈𝑧, 𝑚〉}) ∈ V |
| 68 | | f1oeq1 6836 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑚〉}) → (𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚 ↔ (𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚)) |
| 69 | 67, 68 | spcev 3606 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚 → ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚) |
| 70 | | bren 8995 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∪ {𝑧}) ≈ suc 𝑚 ↔ ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚) |
| 71 | 69, 70 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚 → (𝑥 ∪ {𝑧}) ≈ suc 𝑚) |
| 72 | 64, 71 | sylbir 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚) |
| 73 | 61, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:𝑥–1-1-onto→𝑚 ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚) |
| 74 | 73 | adantll 714 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚) |
| 75 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑥 ∈ V |
| 76 | | snex 5436 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑧} ∈ V |
| 77 | 75, 76 | unex 7764 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∪ {𝑧}) ∈ V |
| 78 | | sseq1 4009 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦 ⊆ 𝐴 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴)) |
| 79 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦 ≈ suc 𝑚 ↔ (𝑥 ∪ {𝑧}) ≈ suc 𝑚)) |
| 80 | 78, 79 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝑥 ∪ {𝑧}) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚) ↔ ((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚))) |
| 81 | 77, 80 | spcev 3606 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)) |
| 82 | 48, 74, 81 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)) |
| 83 | 82 | expcom 413 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω) → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))) |
| 84 | 83 | ex 412 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
| 85 | 84 | exlimiv 1930 |
. . . . . . . . . . . . . 14
⊢
(∃𝑧 𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
| 86 | 42, 85 | sylbi 217 |
. . . . . . . . . . . . 13
⊢ (¬
(𝐴 ∖ 𝑥) = ∅ → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
| 87 | 86 | com13 88 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
| 88 | 87 | expcom 413 |
. . . . . . . . . . 11
⊢ (𝑓:𝑥–1-1-onto→𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))) |
| 89 | 88 | exlimiv 1930 |
. . . . . . . . . 10
⊢
(∃𝑓 𝑓:𝑥–1-1-onto→𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))) |
| 90 | 41, 89 | sylbi 217 |
. . . . . . . . 9
⊢ (𝑥 ≈ 𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))) |
| 91 | 90 | 3imp21 1114 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))) |
| 92 | 40, 91 | syld 47 |
. . . . . . 7
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))) |
| 93 | 92 | 3expia 1122 |
. . . . . 6
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
| 94 | 93 | exlimiv 1930 |
. . . . 5
⊢
(∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
| 95 | 94 | com3l 89 |
. . . 4
⊢ (𝑚 ∈ ω → (¬
𝐴 ∈ Fin →
(∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
| 96 | 3, 6, 13, 24, 95 | finds2 7920 |
. . 3
⊢ (𝑛 ∈ ω → (¬
𝐴 ∈ Fin →
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))) |
| 97 | 96 | com12 32 |
. 2
⊢ (¬
𝐴 ∈ Fin → (𝑛 ∈ ω →
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))) |
| 98 | 97 | ralrimiv 3145 |
1
⊢ (¬
𝐴 ∈ Fin →
∀𝑛 ∈ ω
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)) |