Step | Hyp | Ref
| Expression |
1 | | isfi 8764 |
. . 3
⊢ (𝐴 ∈ Fin ↔ ∃𝑤 ∈ ω 𝐴 ≈ 𝑤) |
2 | | nnon 7718 |
. . . . . 6
⊢ (𝑤 ∈ ω → 𝑤 ∈ On) |
3 | | eleq1w 2821 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (𝑤 ∈ ω ↔ 𝑧 ∈ ω)) |
4 | | breq2 5078 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ 𝑧)) |
5 | 4 | imbi1d 342 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ 𝑧 → 𝜑))) |
6 | 5 | albidv 1923 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) |
7 | 3, 6 | imbi12d 345 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → ((𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑)) ↔ (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)))) |
8 | | rspe 3237 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → ∃𝑤 ∈ ω 𝑦 ≈ 𝑤) |
9 | | isfi 8764 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑦 ≈ 𝑤) |
10 | 8, 9 | sylibr 233 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → 𝑦 ∈ Fin) |
11 | | 19.21v 1942 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥(𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ↔ (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) |
12 | 11 | ralbii 3092 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝑤 ∀𝑥(𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ↔ ∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) |
13 | | ralcom4 3164 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝑤 ∀𝑥(𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ↔ ∀𝑥∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑))) |
14 | 12, 13 | bitr3i 276 |
. . . . . . . . . . . . . 14
⊢
(∀𝑧 ∈
𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) ↔ ∀𝑥∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑))) |
15 | | pssss 4030 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ⊊ 𝑦 → 𝑥 ⊆ 𝑦) |
16 | | ssfi 8956 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ⊆ 𝑦) → 𝑥 ∈ Fin) |
17 | | isfi 8764 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ Fin ↔ ∃𝑧 ∈ ω 𝑥 ≈ 𝑧) |
18 | 16, 17 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ⊆ 𝑦) → ∃𝑧 ∈ ω 𝑥 ≈ 𝑧) |
19 | 10, 15, 18 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ∃𝑧 ∈ ω 𝑥 ≈ 𝑧) |
20 | | ensym 8789 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ≈ 𝑧 → 𝑧 ≈ 𝑥) |
21 | 20 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ≈ 𝑥) |
22 | | php3 8995 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ⊊ 𝑦) → 𝑥 ≺ 𝑦) |
23 | 10, 22 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → 𝑥 ≺ 𝑦) |
24 | | simpllr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑦 ≈ 𝑤) |
25 | | sdomentr 8898 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ≺ 𝑦 ∧ 𝑦 ≈ 𝑤) → 𝑥 ≺ 𝑤) |
26 | 23, 24, 25 | syl2an2r 682 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑥 ≺ 𝑤) |
27 | | ensdomtr 8900 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ≈ 𝑥 ∧ 𝑥 ≺ 𝑤) → 𝑧 ≺ 𝑤) |
28 | 21, 26, 27 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ≺ 𝑤) |
29 | | nnon 7718 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ω → 𝑧 ∈ On) |
30 | 29 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ∈ On) |
31 | 2 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑤 ∈ On) |
32 | | sdomel 8911 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ≺ 𝑤 → 𝑧 ∈ 𝑤)) |
33 | 30, 31, 32 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → (𝑧 ≺ 𝑤 → 𝑧 ∈ 𝑤)) |
34 | 28, 33 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ∈ 𝑤) |
35 | 34 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → 𝑧 ∈ 𝑤)) |
36 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → 𝑥 ≈ 𝑧) |
37 | 35, 36 | jca2 514 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → (𝑧 ∈ 𝑤 ∧ 𝑥 ≈ 𝑧))) |
38 | 37 | reximdv2 3199 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∃𝑧 ∈ ω 𝑥 ≈ 𝑧 → ∃𝑧 ∈ 𝑤 𝑥 ≈ 𝑧)) |
39 | 19, 38 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ∃𝑧 ∈ 𝑤 𝑥 ≈ 𝑧) |
40 | | r19.29 3184 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑧 ∈
𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ ∃𝑧 ∈ 𝑤 𝑥 ≈ 𝑧) → ∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧)) |
41 | 40 | expcom 414 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑧 ∈
𝑤 𝑥 ≈ 𝑧 → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → ∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧))) |
42 | 39, 41 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → ∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧))) |
43 | | ordom 7722 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ Ord
ω |
44 | | ordelss 6282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Ord
ω ∧ 𝑤 ∈
ω) → 𝑤 ⊆
ω) |
45 | 43, 44 | mpan 687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ω → 𝑤 ⊆
ω) |
46 | 45 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → 𝑤 ⊆ ω) |
47 | 46 | sseld 3920 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (𝑧 ∈ 𝑤 → 𝑧 ∈ ω)) |
48 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ω → ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → (𝑥 ≈ 𝑧 → 𝜑))) |
49 | 48 | impd 411 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ω → (((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧) → 𝜑)) |
50 | 47, 49 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (𝑧 ∈ 𝑤 → (((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧) → 𝜑))) |
51 | 50 | rexlimdv 3212 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧) → 𝜑)) |
52 | 42, 51 | syld 47 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → 𝜑)) |
53 | 52 | ex 413 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (𝑥 ⊊ 𝑦 → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → 𝜑))) |
54 | 53 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → (𝑥 ⊊ 𝑦 → 𝜑))) |
55 | 54 | alimdv 1919 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑥∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → ∀𝑥(𝑥 ⊊ 𝑦 → 𝜑))) |
56 | 14, 55 | syl5bi 241 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → ∀𝑥(𝑥 ⊊ 𝑦 → 𝜑))) |
57 | | findcard3.3 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ Fin →
(∀𝑥(𝑥 ⊊ 𝑦 → 𝜑) → 𝜒)) |
58 | 10, 56, 57 | sylsyld 61 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → 𝜒)) |
59 | 58 | impancom 452 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ω ∧
∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) → (𝑦 ≈ 𝑤 → 𝜒)) |
60 | 59 | alrimiv 1930 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ω ∧
∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) → ∀𝑦(𝑦 ≈ 𝑤 → 𝜒)) |
61 | 60 | expcom 414 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → (𝑤 ∈ ω → ∀𝑦(𝑦 ≈ 𝑤 → 𝜒))) |
62 | | breq1 5077 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑤 ↔ 𝑦 ≈ 𝑤)) |
63 | | findcard3.1 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
64 | 62, 63 | imbi12d 345 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑦 ≈ 𝑤 → 𝜒))) |
65 | 64 | cbvalvw 2039 |
. . . . . . . . 9
⊢
(∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑦(𝑦 ≈ 𝑤 → 𝜒)) |
66 | 61, 65 | syl6ibr 251 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → (𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑))) |
67 | 66 | a1i 11 |
. . . . . . 7
⊢ (𝑤 ∈ On → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → (𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑)))) |
68 | 7, 67 | tfis2 7703 |
. . . . . 6
⊢ (𝑤 ∈ On → (𝑤 ∈ ω →
∀𝑥(𝑥 ≈ 𝑤 → 𝜑))) |
69 | 2, 68 | mpcom 38 |
. . . . 5
⊢ (𝑤 ∈ ω →
∀𝑥(𝑥 ≈ 𝑤 → 𝜑)) |
70 | 69 | rgen 3074 |
. . . 4
⊢
∀𝑤 ∈
ω ∀𝑥(𝑥 ≈ 𝑤 → 𝜑) |
71 | | r19.29 3184 |
. . . 4
⊢
((∀𝑤 ∈
ω ∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ ∃𝑤 ∈ ω 𝐴 ≈ 𝑤) → ∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤)) |
72 | 70, 71 | mpan 687 |
. . 3
⊢
(∃𝑤 ∈
ω 𝐴 ≈ 𝑤 → ∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤)) |
73 | 1, 72 | sylbi 216 |
. 2
⊢ (𝐴 ∈ Fin → ∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤)) |
74 | | breq1 5077 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ≈ 𝑤 ↔ 𝐴 ≈ 𝑤)) |
75 | | findcard3.2 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
76 | 74, 75 | imbi12d 345 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝐴 ≈ 𝑤 → 𝜏))) |
77 | 76 | spcgv 3535 |
. . . 4
⊢ (𝐴 ∈ Fin →
(∀𝑥(𝑥 ≈ 𝑤 → 𝜑) → (𝐴 ≈ 𝑤 → 𝜏))) |
78 | 77 | impd 411 |
. . 3
⊢ (𝐴 ∈ Fin →
((∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤) → 𝜏)) |
79 | 78 | rexlimdvw 3219 |
. 2
⊢ (𝐴 ∈ Fin → (∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤) → 𝜏)) |
80 | 73, 79 | mpd 15 |
1
⊢ (𝐴 ∈ Fin → 𝜏) |