Step | Hyp | Ref
| Expression |
1 | | isfi 7865 |
. . 3
⊢ (𝐴 ∈ Fin ↔ ∃𝑤 ∈ ω 𝐴 ≈ 𝑤) |
2 | | nnon 6963 |
. . . . . 6
⊢ (𝑤 ∈ ω → 𝑤 ∈ On) |
3 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (𝑤 ∈ ω ↔ 𝑧 ∈ ω)) |
4 | | breq2 4587 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ 𝑧)) |
5 | 4 | imbi1d 330 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ 𝑧 → 𝜑))) |
6 | 5 | albidv 1836 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) |
7 | 3, 6 | imbi12d 333 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → ((𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑)) ↔ (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)))) |
8 | | rspe 2986 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → ∃𝑤 ∈ ω 𝑦 ≈ 𝑤) |
9 | | isfi 7865 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑦 ≈ 𝑤) |
10 | 8, 9 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → 𝑦 ∈ Fin) |
11 | | 19.21v 1855 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥(𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ↔ (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) |
12 | 11 | ralbii 2963 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝑤 ∀𝑥(𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ↔ ∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) |
13 | | ralcom4 3197 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝑤 ∀𝑥(𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ↔ ∀𝑥∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑))) |
14 | 12, 13 | bitr3i 265 |
. . . . . . . . . . . . . 14
⊢
(∀𝑧 ∈
𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) ↔ ∀𝑥∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑))) |
15 | | pssss 3664 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ⊊ 𝑦 → 𝑥 ⊆ 𝑦) |
16 | | ssfi 8065 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ⊆ 𝑦) → 𝑥 ∈ Fin) |
17 | | isfi 7865 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ Fin ↔ ∃𝑧 ∈ ω 𝑥 ≈ 𝑧) |
18 | 16, 17 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ⊆ 𝑦) → ∃𝑧 ∈ ω 𝑥 ≈ 𝑧) |
19 | 10, 15, 18 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ∃𝑧 ∈ ω 𝑥 ≈ 𝑧) |
20 | | ensym 7891 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ≈ 𝑧 → 𝑧 ≈ 𝑥) |
21 | 20 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ≈ 𝑥) |
22 | | php3 8031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ⊊ 𝑦) → 𝑥 ≺ 𝑦) |
23 | 10, 22 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → 𝑥 ≺ 𝑦) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑥 ≺ 𝑦) |
25 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑦 ≈ 𝑤) |
26 | | sdomentr 7979 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ≺ 𝑦 ∧ 𝑦 ≈ 𝑤) → 𝑥 ≺ 𝑤) |
27 | 24, 25, 26 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑥 ≺ 𝑤) |
28 | | ensdomtr 7981 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ≈ 𝑥 ∧ 𝑥 ≺ 𝑤) → 𝑧 ≺ 𝑤) |
29 | 21, 27, 28 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ≺ 𝑤) |
30 | | nnon 6963 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ω → 𝑧 ∈ On) |
31 | 30 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ∈ On) |
32 | 2 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑤 ∈ On) |
33 | | sdomel 7992 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ≺ 𝑤 → 𝑧 ∈ 𝑤)) |
34 | 31, 32, 33 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → (𝑧 ≺ 𝑤 → 𝑧 ∈ 𝑤)) |
35 | 29, 34 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ∈ 𝑤) |
36 | 35 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → 𝑧 ∈ 𝑤)) |
37 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → 𝑥 ≈ 𝑧) |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → 𝑥 ≈ 𝑧)) |
39 | 36, 38 | jcad 554 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → (𝑧 ∈ 𝑤 ∧ 𝑥 ≈ 𝑧))) |
40 | 39 | reximdv2 2997 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∃𝑧 ∈ ω 𝑥 ≈ 𝑧 → ∃𝑧 ∈ 𝑤 𝑥 ≈ 𝑧)) |
41 | 19, 40 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ∃𝑧 ∈ 𝑤 𝑥 ≈ 𝑧) |
42 | | r19.29 3054 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑧 ∈
𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ ∃𝑧 ∈ 𝑤 𝑥 ≈ 𝑧) → ∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧)) |
43 | 42 | expcom 450 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑧 ∈
𝑤 𝑥 ≈ 𝑧 → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → ∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧))) |
44 | 41, 43 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → ∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧))) |
45 | | ordom 6966 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ Ord
ω |
46 | | ordelss 5656 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Ord
ω ∧ 𝑤 ∈
ω) → 𝑤 ⊆
ω) |
47 | 45, 46 | mpan 702 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ω → 𝑤 ⊆
ω) |
48 | 47 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → 𝑤 ⊆ ω) |
49 | 48 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (𝑧 ∈ 𝑤 → 𝑧 ∈ ω)) |
50 | | pm2.27 41 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ω → ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → (𝑥 ≈ 𝑧 → 𝜑))) |
51 | 50 | impd 446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ω → (((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧) → 𝜑)) |
52 | 49, 51 | syl6 34 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (𝑧 ∈ 𝑤 → (((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧) → 𝜑))) |
53 | 52 | rexlimdv 3012 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧) → 𝜑)) |
54 | 44, 53 | syld 46 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → 𝜑)) |
55 | 54 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (𝑥 ⊊ 𝑦 → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → 𝜑))) |
56 | 55 | com23 84 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → (𝑥 ⊊ 𝑦 → 𝜑))) |
57 | 56 | alimdv 1832 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑥∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → ∀𝑥(𝑥 ⊊ 𝑦 → 𝜑))) |
58 | 14, 57 | syl5bi 231 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → ∀𝑥(𝑥 ⊊ 𝑦 → 𝜑))) |
59 | | findcard3.3 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ Fin →
(∀𝑥(𝑥 ⊊ 𝑦 → 𝜑) → 𝜒)) |
60 | 10, 58, 59 | sylsyld 59 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → 𝜒)) |
61 | 60 | impancom 455 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ω ∧
∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) → (𝑦 ≈ 𝑤 → 𝜒)) |
62 | 61 | alrimiv 1842 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ω ∧
∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) → ∀𝑦(𝑦 ≈ 𝑤 → 𝜒)) |
63 | 62 | expcom 450 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → (𝑤 ∈ ω → ∀𝑦(𝑦 ≈ 𝑤 → 𝜒))) |
64 | | breq1 4586 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑤 ↔ 𝑦 ≈ 𝑤)) |
65 | | findcard3.1 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
66 | 64, 65 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑦 ≈ 𝑤 → 𝜒))) |
67 | 66 | cbvalv 2261 |
. . . . . . . . 9
⊢
(∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑦(𝑦 ≈ 𝑤 → 𝜒)) |
68 | 63, 67 | syl6ibr 241 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → (𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑))) |
69 | 68 | a1i 11 |
. . . . . . 7
⊢ (𝑤 ∈ On → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → (𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑)))) |
70 | 7, 69 | tfis2 6948 |
. . . . . 6
⊢ (𝑤 ∈ On → (𝑤 ∈ ω →
∀𝑥(𝑥 ≈ 𝑤 → 𝜑))) |
71 | 2, 70 | mpcom 37 |
. . . . 5
⊢ (𝑤 ∈ ω →
∀𝑥(𝑥 ≈ 𝑤 → 𝜑)) |
72 | 71 | rgen 2906 |
. . . 4
⊢
∀𝑤 ∈
ω ∀𝑥(𝑥 ≈ 𝑤 → 𝜑) |
73 | | r19.29 3054 |
. . . 4
⊢
((∀𝑤 ∈
ω ∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ ∃𝑤 ∈ ω 𝐴 ≈ 𝑤) → ∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤)) |
74 | 72, 73 | mpan 702 |
. . 3
⊢
(∃𝑤 ∈
ω 𝐴 ≈ 𝑤 → ∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤)) |
75 | 1, 74 | sylbi 206 |
. 2
⊢ (𝐴 ∈ Fin → ∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤)) |
76 | | breq1 4586 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ≈ 𝑤 ↔ 𝐴 ≈ 𝑤)) |
77 | | findcard3.2 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
78 | 76, 77 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝐴 ≈ 𝑤 → 𝜏))) |
79 | 78 | spcgv 3266 |
. . . 4
⊢ (𝐴 ∈ Fin →
(∀𝑥(𝑥 ≈ 𝑤 → 𝜑) → (𝐴 ≈ 𝑤 → 𝜏))) |
80 | 79 | impd 446 |
. . 3
⊢ (𝐴 ∈ Fin →
((∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤) → 𝜏)) |
81 | 80 | rexlimdvw 3016 |
. 2
⊢ (𝐴 ∈ Fin → (∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤) → 𝜏)) |
82 | 75, 81 | mpd 15 |
1
⊢ (𝐴 ∈ Fin → 𝜏) |