Step | Hyp | Ref
| Expression |
1 | | nfe1 2027 |
. . . . 5
⊢
Ⅎ𝑥∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑) |
2 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑥ω |
3 | 1, 2 | nfrab 3123 |
. . . 4
⊢
Ⅎ𝑥{𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} |
4 | | nfcv 2764 |
. . . 4
⊢
Ⅎ𝑥∅ |
5 | 3, 4 | nfne 2894 |
. . 3
⊢
Ⅎ𝑥{𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅ |
6 | | isfi 7979 |
. . . 4
⊢ (𝑥 ∈ Fin ↔ ∃𝑚 ∈ ω 𝑥 ≈ 𝑚) |
7 | | 19.8a 2052 |
. . . . . . . . . 10
⊢ ((𝑥 ≈ 𝑚 ∧ 𝜑) → ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)) |
8 | 7 | anim2i 593 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ω ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑))) |
9 | 8 | 3impb 1260 |
. . . . . . . 8
⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑) → (𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑))) |
10 | | breq2 4657 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑚)) |
11 | 10 | anbi1d 741 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → ((𝑥 ≈ 𝑛 ∧ 𝜑) ↔ (𝑥 ≈ 𝑚 ∧ 𝜑))) |
12 | 11 | exbidv 1850 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑) ↔ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑))) |
13 | 12 | elrab 3363 |
. . . . . . . 8
⊢ (𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ↔ (𝑚 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑))) |
14 | 9, 13 | sylibr 224 |
. . . . . . 7
⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑) → 𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)}) |
15 | | ne0i 3921 |
. . . . . . 7
⊢ (𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅) |
16 | 14, 15 | syl 17 |
. . . . . 6
⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚 ∧ 𝜑) → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅) |
17 | 16 | 3exp 1264 |
. . . . 5
⊢ (𝑚 ∈ ω → (𝑥 ≈ 𝑚 → (𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅))) |
18 | 17 | rexlimiv 3027 |
. . . 4
⊢
(∃𝑚 ∈
ω 𝑥 ≈ 𝑚 → (𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅)) |
19 | 6, 18 | sylbi 207 |
. . 3
⊢ (𝑥 ∈ Fin → (𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅)) |
20 | 5, 19 | rexlimi 3024 |
. 2
⊢
(∃𝑥 ∈ Fin
𝜑 → {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅) |
21 | | epweon 6983 |
. . 3
⊢ E We
On |
22 | | ssrab2 3687 |
. . . 4
⊢ {𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ⊆ ω |
23 | | omsson 7069 |
. . . 4
⊢ ω
⊆ On |
24 | 22, 23 | sstri 3612 |
. . 3
⊢ {𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ⊆ On |
25 | | wefrc 5108 |
. . 3
⊢ (( E We
On ∧ {𝑛 ∈ ω
∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ⊆ On ∧ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅) → ∃𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) |
26 | 21, 24, 25 | mp3an12 1414 |
. 2
⊢ ({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ≠ ∅ → ∃𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) |
27 | | nfv 1843 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑚 ∈ ω |
28 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑚 |
29 | 3, 28 | nfin 3820 |
. . . . . . . 8
⊢
Ⅎ𝑥({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) |
30 | 29 | nfeq1 2778 |
. . . . . . 7
⊢
Ⅎ𝑥({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ |
31 | 27, 30 | nfan 1828 |
. . . . . 6
⊢
Ⅎ𝑥(𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) |
32 | | simprr 796 |
. . . . . . . 8
⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → 𝜑) |
33 | | sspss 3706 |
. . . . . . . . . . . . 13
⊢ (𝑦 ⊆ 𝑥 ↔ (𝑦 ⊊ 𝑥 ∨ 𝑦 = 𝑥)) |
34 | | rspe 3003 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚) → ∃𝑚 ∈ ω 𝑥 ≈ 𝑚) |
35 | | pssss 3702 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ⊊ 𝑥 → 𝑦 ⊆ 𝑥) |
36 | | ssfi 8180 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥) → 𝑦 ∈ Fin) |
37 | 35, 36 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ Fin ∧ 𝑦 ⊊ 𝑥) → 𝑦 ∈ Fin) |
38 | 37 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ Fin → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin)) |
39 | 6, 38 | sylbir 225 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∃𝑚 ∈
ω 𝑥 ≈ 𝑚 → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin)) |
40 | 34, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚) → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin)) |
41 | 40 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑚 ∈ ω ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin)) |
42 | 41 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → 𝑦 ∈ Fin)) |
43 | | isfi 7979 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ Fin ↔ ∃𝑘 ∈ ω 𝑦 ≈ 𝑘) |
44 | | simprll 802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑘 ∈ ω) |
45 | | simprlr 803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑦 ≈ 𝑘) |
46 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝜓) |
47 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 𝑦 ∈ V |
48 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑘 ↔ 𝑦 ≈ 𝑘)) |
49 | | finminlem.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
50 | 48, 49 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑘 ∧ 𝜑) ↔ (𝑦 ≈ 𝑘 ∧ 𝜓))) |
51 | 47, 50 | spcev 3300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ≈ 𝑘 ∧ 𝜓) → ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) |
52 | 45, 46, 51 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) |
53 | 34, 6 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑚 ∈ ω ∧ 𝑥 ≈ 𝑚) → 𝑥 ∈ Fin) |
54 | 53 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑚 ∈ ω ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → 𝑥 ∈ Fin) |
55 | 54 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → 𝑥 ∈ Fin) |
56 | 55 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → 𝑥 ∈ Fin) |
57 | | php3 8146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑥 ∈ Fin ∧ 𝑦 ⊊ 𝑥) → 𝑦 ≺ 𝑥) |
58 | 57 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ Fin → (𝑦 ⊊ 𝑥 → 𝑦 ≺ 𝑥)) |
59 | 56, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑦 ⊊ 𝑥 → 𝑦 ≺ 𝑥)) |
60 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 𝑘 ∈ V |
61 | | ssdomg 8001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑘 ∈ V → (𝑚 ⊆ 𝑘 → 𝑚 ≼ 𝑘)) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑚 ⊆ 𝑘 → 𝑚 ≼ 𝑘) |
63 | | endomtr 8014 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑥 ≈ 𝑚 ∧ 𝑚 ≼ 𝑘) → 𝑥 ≼ 𝑘) |
64 | 63 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑥 ≈ 𝑚 → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘)) |
65 | 64 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓) → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘)) |
66 | 65 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑘)) |
67 | | ensym 8005 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 ≈ 𝑘 → 𝑘 ≈ 𝑦) |
68 | | domentr 8015 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑥 ≼ 𝑘 ∧ 𝑘 ≈ 𝑦) → 𝑥 ≼ 𝑦) |
69 | 67, 68 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑥 ≼ 𝑘 ∧ 𝑦 ≈ 𝑘) → 𝑥 ≼ 𝑦) |
70 | 69 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 ≈ 𝑘 → (𝑥 ≼ 𝑘 → 𝑥 ≼ 𝑦)) |
71 | 70 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑥 ≼ 𝑘 → 𝑥 ≼ 𝑦)) |
72 | 66, 71 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑚 ≼ 𝑘 → 𝑥 ≼ 𝑦)) |
73 | 62, 72 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑚 ⊆ 𝑘 → 𝑥 ≼ 𝑦)) |
74 | | domnsym 8086 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 ≼ 𝑦 → ¬ 𝑦 ≺ 𝑥) |
75 | 74 | con2i 134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ≺ 𝑥 → ¬ 𝑥 ≼ 𝑦) |
76 | 73, 75 | nsyli 155 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑦 ≺ 𝑥 → ¬ 𝑚 ⊆ 𝑘)) |
77 | 59, 76 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ (𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘)) → (𝑦 ⊊ 𝑥 → ¬ 𝑚 ⊆ 𝑘)) |
78 | 77 | impr 649 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ¬ 𝑚 ⊆ 𝑘) |
79 | | nnord 7073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑚 ∈ ω → Ord 𝑚) |
80 | 79 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → Ord 𝑚) |
81 | | nnord 7073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 ∈ ω → Ord 𝑘) |
82 | 81 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) → Ord 𝑘) |
83 | 82 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → Ord 𝑘) |
84 | | ordtri1 5756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((Ord
𝑚 ∧ Ord 𝑘) → (𝑚 ⊆ 𝑘 ↔ ¬ 𝑘 ∈ 𝑚)) |
85 | 84 | con2bid 344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((Ord
𝑚 ∧ Ord 𝑘) → (𝑘 ∈ 𝑚 ↔ ¬ 𝑚 ⊆ 𝑘)) |
86 | 80, 83, 85 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → (𝑘 ∈ 𝑚 ↔ ¬ 𝑚 ⊆ 𝑘)) |
87 | 78, 86 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑘 ∈ 𝑚) |
88 | 44, 52, 87 | jca31 557 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ((𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) ∧ 𝑘 ∈ 𝑚)) |
89 | | elin 3796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ↔ (𝑘 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∧ 𝑘 ∈ 𝑚)) |
90 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑛 = 𝑘 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑘)) |
91 | 90 | anbi1d 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑛 = 𝑘 → ((𝑥 ≈ 𝑛 ∧ 𝜑) ↔ (𝑥 ≈ 𝑘 ∧ 𝜑))) |
92 | 91 | exbidv 1850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 = 𝑘 → (∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑) ↔ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑))) |
93 | 92 | elrab 3363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ↔ (𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑))) |
94 | 93 | anbi1i 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑘 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∧ 𝑘 ∈ 𝑚) ↔ ((𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) ∧ 𝑘 ∈ 𝑚)) |
95 | 89, 94 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ↔ ((𝑘 ∈ ω ∧ ∃𝑥(𝑥 ≈ 𝑘 ∧ 𝜑)) ∧ 𝑘 ∈ 𝑚)) |
96 | 88, 95 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → 𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚)) |
97 | | ne0i 3921 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) ∧ ((𝑘 ∈ ω ∧ 𝑦 ≈ 𝑘) ∧ 𝑦 ⊊ 𝑥)) → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅) |
99 | 98 | exp44 641 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑘 ∈ ω → (𝑦 ≈ 𝑘 → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)))) |
100 | 99 | rexlimdv 3030 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (∃𝑘 ∈ ω 𝑦 ≈ 𝑘 → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅))) |
101 | 43, 100 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ∈ Fin → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅))) |
102 | 101 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → (𝑦 ∈ Fin → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅))) |
103 | 42, 102 | mpdd 43 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) ≠ ∅)) |
104 | 103 | necon2bd 2810 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ∈ ω ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ¬ 𝑦 ⊊ 𝑥)) |
105 | 104 | ex 450 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ω → (((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓) → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ¬ 𝑦 ⊊ 𝑥))) |
106 | 105 | com23 86 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ω → (({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → (((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓) → ¬ 𝑦 ⊊ 𝑥))) |
107 | 106 | imp31 448 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → ¬ 𝑦 ⊊ 𝑥) |
108 | 107 | pm2.21d 118 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊊ 𝑥 → 𝑥 = 𝑦)) |
109 | | equcomi 1944 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦) |
110 | 109 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 = 𝑥 → 𝑥 = 𝑦)) |
111 | 108, 110 | jaod 395 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → ((𝑦 ⊊ 𝑥 ∨ 𝑦 = 𝑥) → 𝑥 = 𝑦)) |
112 | 33, 111 | syl5bi 232 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ ((𝑥 ≈ 𝑚 ∧ 𝜑) ∧ 𝜓)) → (𝑦 ⊆ 𝑥 → 𝑥 = 𝑦)) |
113 | 112 | expr 643 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝜓 → (𝑦 ⊆ 𝑥 → 𝑥 = 𝑦))) |
114 | 113 | com23 86 |
. . . . . . . . . 10
⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝑦 ⊆ 𝑥 → (𝜓 → 𝑥 = 𝑦))) |
115 | 114 | impd 447 |
. . . . . . . . 9
⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → ((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)) |
116 | 115 | alrimiv 1855 |
. . . . . . . 8
⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)) |
117 | 32, 116 | jca 554 |
. . . . . . 7
⊢ (((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) ∧ (𝑥 ≈ 𝑚 ∧ 𝜑)) → (𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))) |
118 | 117 | ex 450 |
. . . . . 6
⊢ ((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) → ((𝑥 ≈ 𝑚 ∧ 𝜑) → (𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))) |
119 | 31, 118 | eximd 2085 |
. . . . 5
⊢ ((𝑚 ∈ ω ∧ ({𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅) → (∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑) → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))) |
120 | 119 | impancom 456 |
. . . 4
⊢ ((𝑚 ∈ ω ∧
∃𝑥(𝑥 ≈ 𝑚 ∧ 𝜑)) → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))) |
121 | 13, 120 | sylbi 207 |
. . 3
⊢ (𝑚 ∈ {𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} → (({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))) |
122 | 121 | rexlimiv 3027 |
. 2
⊢
(∃𝑚 ∈
{𝑛 ∈ ω ∣
∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ({𝑛 ∈ ω ∣ ∃𝑥(𝑥 ≈ 𝑛 ∧ 𝜑)} ∩ 𝑚) = ∅ → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))) |
123 | 20, 26, 122 | 3syl 18 |
1
⊢
(∃𝑥 ∈ Fin
𝜑 → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))) |