Step | Hyp | Ref
| Expression |
1 | | breq2 5109 |
. . . . . 6
⊢ (𝑛 = ∅ → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ ∅)) |
2 | 1 | anbi2d 629 |
. . . . 5
⊢ (𝑛 = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅))) |
3 | 2 | exbidv 1924 |
. . . 4
⊢ (𝑛 = ∅ → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅))) |
4 | | breq2 5109 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑚)) |
5 | 4 | anbi2d 629 |
. . . . 5
⊢ (𝑛 = 𝑚 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚))) |
6 | 5 | exbidv 1924 |
. . . 4
⊢ (𝑛 = 𝑚 → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚))) |
7 | | sseq1 3969 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
8 | 7 | adantl 482 |
. . . . . 6
⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
9 | | breq1 5108 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑛 ↔ 𝑦 ≈ 𝑛)) |
10 | | breq2 5109 |
. . . . . . 7
⊢ (𝑛 = suc 𝑚 → (𝑦 ≈ 𝑛 ↔ 𝑦 ≈ suc 𝑚)) |
11 | 9, 10 | sylan9bbr 511 |
. . . . . 6
⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → (𝑥 ≈ 𝑛 ↔ 𝑦 ≈ suc 𝑚)) |
12 | 8, 11 | anbi12d 631 |
. . . . 5
⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))) |
13 | 12 | cbvexdvaw 2042 |
. . . 4
⊢ (𝑛 = suc 𝑚 → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))) |
14 | | 0ss 4356 |
. . . . . 6
⊢ ∅
⊆ 𝐴 |
15 | | peano1 7825 |
. . . . . . 7
⊢ ∅
∈ ω |
16 | | enrefnn 8991 |
. . . . . . 7
⊢ (∅
∈ ω → ∅ ≈ ∅) |
17 | 15, 16 | ax-mp 5 |
. . . . . 6
⊢ ∅
≈ ∅ |
18 | | 0ex 5264 |
. . . . . . 7
⊢ ∅
∈ V |
19 | | sseq1 3969 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
20 | | breq1 5108 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑥 ≈ ∅ ↔ ∅
≈ ∅)) |
21 | 19, 20 | anbi12d 631 |
. . . . . . 7
⊢ (𝑥 = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅) ↔ (∅ ⊆
𝐴 ∧ ∅ ≈
∅))) |
22 | 18, 21 | spcev 3565 |
. . . . . 6
⊢ ((∅
⊆ 𝐴 ∧ ∅
≈ ∅) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅)) |
23 | 14, 17, 22 | mp2an 690 |
. . . . 5
⊢
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅) |
24 | 23 | a1i 11 |
. . . 4
⊢ (¬
𝐴 ∈ Fin →
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅)) |
25 | | ssdif0 4323 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ 𝑥 ↔ (𝐴 ∖ 𝑥) = ∅) |
26 | | eqss 3959 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐴 ↔ (𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥)) |
27 | | breq1 5108 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝐴 → (𝑥 ≈ 𝑚 ↔ 𝐴 ≈ 𝑚)) |
28 | 27 | biimpa 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚) → 𝐴 ≈ 𝑚) |
29 | | rspe 3232 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ∈ ω ∧ 𝐴 ≈ 𝑚) → ∃𝑚 ∈ ω 𝐴 ≈ 𝑚) |
30 | 28, 29 | sylan2 593 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ω ∧ (𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚)) → ∃𝑚 ∈ ω 𝐴 ≈ 𝑚) |
31 | | isfi 8916 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ Fin ↔ ∃𝑚 ∈ ω 𝐴 ≈ 𝑚) |
32 | 30, 31 | sylibr 233 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ω ∧ (𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚)) → 𝐴 ∈ Fin) |
33 | 32 | expcom 414 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin)) |
34 | 26, 33 | sylanbr 582 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥) ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin)) |
35 | 34 | ex 413 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥) → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin))) |
36 | 25, 35 | sylan2br 595 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ 𝐴 ∧ (𝐴 ∖ 𝑥) = ∅) → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin))) |
37 | 36 | expcom 414 |
. . . . . . . . . . 11
⊢ ((𝐴 ∖ 𝑥) = ∅ → (𝑥 ⊆ 𝐴 → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin)))) |
38 | 37 | 3impd 1348 |
. . . . . . . . . 10
⊢ ((𝐴 ∖ 𝑥) = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → 𝐴 ∈ Fin)) |
39 | 38 | com12 32 |
. . . . . . . . 9
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → ((𝐴 ∖ 𝑥) = ∅ → 𝐴 ∈ Fin)) |
40 | 39 | con3d 152 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ¬ (𝐴 ∖ 𝑥) = ∅)) |
41 | | bren 8893 |
. . . . . . . . . 10
⊢ (𝑥 ≈ 𝑚 ↔ ∃𝑓 𝑓:𝑥–1-1-onto→𝑚) |
42 | | neq0 4305 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝐴 ∖ 𝑥) = ∅ ↔ ∃𝑧 𝑧 ∈ (𝐴 ∖ 𝑥)) |
43 | | eldifi 4086 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → 𝑧 ∈ 𝐴) |
44 | 43 | snssd 4769 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → {𝑧} ⊆ 𝐴) |
45 | | unss 4144 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴) ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴) |
46 | 45 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴) → (𝑥 ∪ {𝑧}) ⊆ 𝐴) |
47 | 44, 46 | sylan2 593 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑥)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴) |
48 | 47 | ad2ant2r 745 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴) |
49 | | vex 3449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑧 ∈ V |
50 | | vex 3449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑚 ∈ V |
51 | 49, 50 | f1osn 6824 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
{〈𝑧, 𝑚〉}:{𝑧}–1-1-onto→{𝑚} |
52 | 51 | jctr 525 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓:𝑥–1-1-onto→𝑚 → (𝑓:𝑥–1-1-onto→𝑚 ∧ {〈𝑧, 𝑚〉}:{𝑧}–1-1-onto→{𝑚})) |
53 | | eldifn 4087 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → ¬ 𝑧 ∈ 𝑥) |
54 | | disjsn 4672 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑥) |
55 | 53, 54 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑥 ∩ {𝑧}) = ∅) |
56 | | nnord 7810 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ω → Ord 𝑚) |
57 | | orddisj 6355 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Ord
𝑚 → (𝑚 ∩ {𝑚}) = ∅) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ω → (𝑚 ∩ {𝑚}) = ∅) |
59 | 55, 58 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω) → ((𝑥 ∩ {𝑧}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅)) |
60 | | f1oun 6803 |
. . . . . . . . . . . . . . . . . . . . 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 6323 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ suc 𝑚 = (𝑚 ∪ {𝑚}) |
63 | | f1oeq3 6774 |
. . . . . . . . . . . . . . . . . . . . . 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 3449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑓 ∈ V |
66 | | snex 5388 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
{〈𝑧, 𝑚〉} ∈
V |
67 | 65, 66 | unex 7680 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∪ {〈𝑧, 𝑚〉}) ∈ V |
68 | | f1oeq1 6772 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑚〉}) → (𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚 ↔ (𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚)) |
69 | 67, 68 | spcev 3565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚 → ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚) |
70 | | bren 8893 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∪ {𝑧}) ≈ suc 𝑚 ↔ ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚) |
71 | 69, 70 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚 → (𝑥 ∪ {𝑧}) ≈ suc 𝑚) |
72 | 64, 71 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚) |
73 | 61, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:𝑥–1-1-onto→𝑚 ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚) |
74 | 73 | adantll 712 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚) |
75 | | vex 3449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑥 ∈ V |
76 | | snex 5388 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑧} ∈ V |
77 | 75, 76 | unex 7680 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∪ {𝑧}) ∈ V |
78 | | sseq1 3969 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦 ⊆ 𝐴 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴)) |
79 | | breq1 5108 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦 ≈ suc 𝑚 ↔ (𝑥 ∪ {𝑧}) ≈ suc 𝑚)) |
80 | 78, 79 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝑥 ∪ {𝑧}) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚) ↔ ((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚))) |
81 | 77, 80 | spcev 3565 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)) |
82 | 48, 74, 81 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)) |
83 | 82 | expcom 414 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω) → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))) |
84 | 83 | ex 413 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
85 | 84 | exlimiv 1933 |
. . . . . . . . . . . . . 14
⊢
(∃𝑧 𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
86 | 42, 85 | sylbi 216 |
. . . . . . . . . . . . 13
⊢ (¬
(𝐴 ∖ 𝑥) = ∅ → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
87 | 86 | com13 88 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
88 | 87 | expcom 414 |
. . . . . . . . . . 11
⊢ (𝑓:𝑥–1-1-onto→𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))) |
89 | 88 | exlimiv 1933 |
. . . . . . . . . 10
⊢
(∃𝑓 𝑓:𝑥–1-1-onto→𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))) |
90 | 41, 89 | sylbi 216 |
. . . . . . . . 9
⊢ (𝑥 ≈ 𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))) |
91 | 90 | 3imp21 1114 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))) |
92 | 40, 91 | syld 47 |
. . . . . . 7
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))) |
93 | 92 | 3expia 1121 |
. . . . . 6
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
94 | 93 | exlimiv 1933 |
. . . . 5
⊢
(∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
95 | 94 | com3l 89 |
. . . 4
⊢ (𝑚 ∈ ω → (¬
𝐴 ∈ Fin →
(∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
96 | 3, 6, 13, 24, 95 | finds2 7837 |
. . 3
⊢ (𝑛 ∈ ω → (¬
𝐴 ∈ Fin →
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))) |
97 | 96 | com12 32 |
. 2
⊢ (¬
𝐴 ∈ Fin → (𝑛 ∈ ω →
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))) |
98 | 97 | ralrimiv 3142 |
1
⊢ (¬
𝐴 ∈ Fin →
∀𝑛 ∈ ω
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)) |