Step | Hyp | Ref
| Expression |
1 | | breq2 5078 |
. . . . . 6
⊢ (𝑛 = ∅ → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ ∅)) |
2 | 1 | anbi2d 629 |
. . . . 5
⊢ (𝑛 = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅))) |
3 | 2 | exbidv 1924 |
. . . 4
⊢ (𝑛 = ∅ → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅))) |
4 | | breq2 5078 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑚)) |
5 | 4 | anbi2d 629 |
. . . . 5
⊢ (𝑛 = 𝑚 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚))) |
6 | 5 | exbidv 1924 |
. . . 4
⊢ (𝑛 = 𝑚 → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚))) |
7 | | sseq1 3946 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
8 | 7 | adantl 482 |
. . . . . 6
⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
9 | | breq1 5077 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑛 ↔ 𝑦 ≈ 𝑛)) |
10 | | breq2 5078 |
. . . . . . 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 4330 |
. . . . . 6
⊢ ∅
⊆ 𝐴 |
15 | | 0ex 5231 |
. . . . . . 7
⊢ ∅
∈ V |
16 | 15 | enref 8773 |
. . . . . 6
⊢ ∅
≈ ∅ |
17 | | sseq1 3946 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
18 | | breq1 5077 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑥 ≈ ∅ ↔ ∅
≈ ∅)) |
19 | 17, 18 | anbi12d 631 |
. . . . . . 7
⊢ (𝑥 = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅) ↔ (∅ ⊆
𝐴 ∧ ∅ ≈
∅))) |
20 | 15, 19 | spcev 3545 |
. . . . . 6
⊢ ((∅
⊆ 𝐴 ∧ ∅
≈ ∅) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅)) |
21 | 14, 16, 20 | mp2an 689 |
. . . . 5
⊢
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅) |
22 | 21 | a1i 11 |
. . . 4
⊢ (¬
𝐴 ∈ Fin →
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅)) |
23 | | ssdif0 4297 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ 𝑥 ↔ (𝐴 ∖ 𝑥) = ∅) |
24 | | eqss 3936 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐴 ↔ (𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥)) |
25 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝐴 → (𝑥 ≈ 𝑚 ↔ 𝐴 ≈ 𝑚)) |
26 | 25 | biimpa 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚) → 𝐴 ≈ 𝑚) |
27 | | rspe 3237 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ∈ ω ∧ 𝐴 ≈ 𝑚) → ∃𝑚 ∈ ω 𝐴 ≈ 𝑚) |
28 | 26, 27 | sylan2 593 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ω ∧ (𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚)) → ∃𝑚 ∈ ω 𝐴 ≈ 𝑚) |
29 | | isfi 8764 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ Fin ↔ ∃𝑚 ∈ ω 𝐴 ≈ 𝑚) |
30 | 28, 29 | sylibr 233 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ω ∧ (𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚)) → 𝐴 ∈ Fin) |
31 | 30 | expcom 414 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin)) |
32 | 24, 31 | sylanbr 582 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥) ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin)) |
33 | 32 | ex 413 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥) → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin))) |
34 | 23, 33 | sylan2br 595 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ 𝐴 ∧ (𝐴 ∖ 𝑥) = ∅) → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin))) |
35 | 34 | expcom 414 |
. . . . . . . . . . 11
⊢ ((𝐴 ∖ 𝑥) = ∅ → (𝑥 ⊆ 𝐴 → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin)))) |
36 | 35 | 3impd 1347 |
. . . . . . . . . 10
⊢ ((𝐴 ∖ 𝑥) = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → 𝐴 ∈ Fin)) |
37 | 36 | com12 32 |
. . . . . . . . 9
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → ((𝐴 ∖ 𝑥) = ∅ → 𝐴 ∈ Fin)) |
38 | 37 | con3d 152 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ¬ (𝐴 ∖ 𝑥) = ∅)) |
39 | | bren 8743 |
. . . . . . . . . 10
⊢ (𝑥 ≈ 𝑚 ↔ ∃𝑓 𝑓:𝑥–1-1-onto→𝑚) |
40 | | neq0 4279 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝐴 ∖ 𝑥) = ∅ ↔ ∃𝑧 𝑧 ∈ (𝐴 ∖ 𝑥)) |
41 | | eldifi 4061 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → 𝑧 ∈ 𝐴) |
42 | 41 | snssd 4742 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → {𝑧} ⊆ 𝐴) |
43 | | unss 4118 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴) ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴) |
44 | 43 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴) → (𝑥 ∪ {𝑧}) ⊆ 𝐴) |
45 | 42, 44 | sylan2 593 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑥)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴) |
46 | 45 | ad2ant2r 744 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴) |
47 | | vex 3436 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑧 ∈ V |
48 | | vex 3436 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑚 ∈ V |
49 | 47, 48 | f1osn 6756 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
{〈𝑧, 𝑚〉}:{𝑧}–1-1-onto→{𝑚} |
50 | 49 | jctr 525 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓:𝑥–1-1-onto→𝑚 → (𝑓:𝑥–1-1-onto→𝑚 ∧ {〈𝑧, 𝑚〉}:{𝑧}–1-1-onto→{𝑚})) |
51 | | eldifn 4062 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → ¬ 𝑧 ∈ 𝑥) |
52 | | disjsn 4647 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑥) |
53 | 51, 52 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑥 ∩ {𝑧}) = ∅) |
54 | | nnord 7720 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ω → Ord 𝑚) |
55 | | orddisj 6304 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Ord
𝑚 → (𝑚 ∩ {𝑚}) = ∅) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ω → (𝑚 ∩ {𝑚}) = ∅) |
57 | 53, 56 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω) → ((𝑥 ∩ {𝑧}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅)) |
58 | | f1oun 6735 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑓:𝑥–1-1-onto→𝑚 ∧ {〈𝑧, 𝑚〉}:{𝑧}–1-1-onto→{𝑚}) ∧ ((𝑥 ∩ {𝑧}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅)) → (𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚})) |
59 | 50, 57, 58 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓:𝑥–1-1-onto→𝑚 ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚})) |
60 | | df-suc 6272 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ suc 𝑚 = (𝑚 ∪ {𝑚}) |
61 | | f1oeq3 6706 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (suc
𝑚 = (𝑚 ∪ {𝑚}) → ((𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚 ↔ (𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚 ↔ (𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚})) |
63 | | vex 3436 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑓 ∈ V |
64 | | snex 5354 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
{〈𝑧, 𝑚〉} ∈
V |
65 | 63, 64 | unex 7596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∪ {〈𝑧, 𝑚〉}) ∈ V |
66 | | f1oeq1 6704 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑚〉}) → (𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚 ↔ (𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚)) |
67 | 65, 66 | spcev 3545 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚 → ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚) |
68 | | bren 8743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∪ {𝑧}) ≈ suc 𝑚 ↔ ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚) |
69 | 67, 68 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→suc
𝑚 → (𝑥 ∪ {𝑧}) ≈ suc 𝑚) |
70 | 62, 69 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∪ {〈𝑧, 𝑚〉}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚) |
71 | 59, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:𝑥–1-1-onto→𝑚 ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚) |
72 | 71 | adantll 711 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚) |
73 | | vex 3436 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑥 ∈ V |
74 | | snex 5354 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑧} ∈ V |
75 | 73, 74 | unex 7596 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∪ {𝑧}) ∈ V |
76 | | sseq1 3946 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦 ⊆ 𝐴 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴)) |
77 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦 ≈ suc 𝑚 ↔ (𝑥 ∪ {𝑧}) ≈ suc 𝑚)) |
78 | 76, 77 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝑥 ∪ {𝑧}) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚) ↔ ((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚))) |
79 | 75, 78 | spcev 3545 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)) |
80 | 46, 72, 79 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)) |
81 | 80 | expcom 414 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω) → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))) |
82 | 81 | ex 413 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
83 | 82 | exlimiv 1933 |
. . . . . . . . . . . . . 14
⊢
(∃𝑧 𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
84 | 40, 83 | sylbi 216 |
. . . . . . . . . . . . 13
⊢ (¬
(𝐴 ∖ 𝑥) = ∅ → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
85 | 84 | com13 88 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
86 | 85 | expcom 414 |
. . . . . . . . . . 11
⊢ (𝑓:𝑥–1-1-onto→𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))) |
87 | 86 | exlimiv 1933 |
. . . . . . . . . 10
⊢
(∃𝑓 𝑓:𝑥–1-1-onto→𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))) |
88 | 39, 87 | sylbi 216 |
. . . . . . . . 9
⊢ (𝑥 ≈ 𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))) |
89 | 88 | 3imp21 1113 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))) |
90 | 38, 89 | syld 47 |
. . . . . . 7
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))) |
91 | 90 | 3expia 1120 |
. . . . . 6
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
92 | 91 | exlimiv 1933 |
. . . . 5
⊢
(∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
93 | 92 | com3l 89 |
. . . 4
⊢ (𝑚 ∈ ω → (¬
𝐴 ∈ Fin →
(∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))) |
94 | 3, 6, 13, 22, 93 | finds2 7747 |
. . 3
⊢ (𝑛 ∈ ω → (¬
𝐴 ∈ Fin →
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))) |
95 | 94 | com12 32 |
. 2
⊢ (¬
𝐴 ∈ Fin → (𝑛 ∈ ω →
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))) |
96 | 95 | ralrimiv 3102 |
1
⊢ (¬
𝐴 ∈ Fin →
∀𝑛 ∈ ω
∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)) |