Step | Hyp | Ref
| Expression |
1 | | isfi 8246 |
. . 3
⊢ (𝐴 ∈ Fin ↔ ∃𝑤 ∈ ω 𝐴 ≈ 𝑤) |
2 | | nnon 7332 |
. . . . . 6
⊢ (𝑤 ∈ ω → 𝑤 ∈ On) |
3 | | eleq1w 2889 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (𝑤 ∈ ω ↔ 𝑧 ∈ ω)) |
4 | | breq2 4877 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ 𝑧)) |
5 | 4 | imbi1d 333 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ 𝑧 → 𝜑))) |
6 | 5 | albidv 2019 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) |
7 | 3, 6 | imbi12d 336 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → ((𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑)) ↔ (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)))) |
8 | | rspe 3211 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → ∃𝑤 ∈ ω 𝑦 ≈ 𝑤) |
9 | | isfi 8246 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑦 ≈ 𝑤) |
10 | 8, 9 | sylibr 226 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → 𝑦 ∈ Fin) |
11 | | 19.21v 2038 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥(𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ↔ (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) |
12 | 11 | ralbii 3189 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝑤 ∀𝑥(𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ↔ ∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) |
13 | | ralcom4 3441 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝑤 ∀𝑥(𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ↔ ∀𝑥∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑))) |
14 | 12, 13 | bitr3i 269 |
. . . . . . . . . . . . . 14
⊢
(∀𝑧 ∈
𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) ↔ ∀𝑥∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑))) |
15 | | pssss 3928 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ⊊ 𝑦 → 𝑥 ⊆ 𝑦) |
16 | | ssfi 8449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ⊆ 𝑦) → 𝑥 ∈ Fin) |
17 | | isfi 8246 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ Fin ↔ ∃𝑧 ∈ ω 𝑥 ≈ 𝑧) |
18 | 16, 17 | sylib 210 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ⊆ 𝑦) → ∃𝑧 ∈ ω 𝑥 ≈ 𝑧) |
19 | 10, 15, 18 | syl2an 589 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ∃𝑧 ∈ ω 𝑥 ≈ 𝑧) |
20 | | ensym 8271 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ≈ 𝑧 → 𝑧 ≈ 𝑥) |
21 | 20 | ad2antll 720 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ≈ 𝑥) |
22 | | php3 8415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ⊊ 𝑦) → 𝑥 ≺ 𝑦) |
23 | 10, 22 | sylan 575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → 𝑥 ≺ 𝑦) |
24 | 23 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑥 ≺ 𝑦) |
25 | | simpllr 793 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑦 ≈ 𝑤) |
26 | | sdomentr 8363 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ≺ 𝑦 ∧ 𝑦 ≈ 𝑤) → 𝑥 ≺ 𝑤) |
27 | 24, 25, 26 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑥 ≺ 𝑤) |
28 | | ensdomtr 8365 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ≈ 𝑥 ∧ 𝑥 ≺ 𝑤) → 𝑧 ≺ 𝑤) |
29 | 21, 27, 28 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ≺ 𝑤) |
30 | | nnon 7332 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ω → 𝑧 ∈ On) |
31 | 30 | ad2antrl 719 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ∈ On) |
32 | 2 | ad3antrrr 721 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑤 ∈ On) |
33 | | sdomel 8376 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ≺ 𝑤 → 𝑧 ∈ 𝑤)) |
34 | 31, 32, 33 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → (𝑧 ≺ 𝑤 → 𝑧 ∈ 𝑤)) |
35 | 29, 34 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ∈ 𝑤) |
36 | 35 | ex 403 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → 𝑧 ∈ 𝑤)) |
37 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → 𝑥 ≈ 𝑧) |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → 𝑥 ≈ 𝑧)) |
39 | 36, 38 | jcad 508 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → (𝑧 ∈ 𝑤 ∧ 𝑥 ≈ 𝑧))) |
40 | 39 | reximdv2 3222 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∃𝑧 ∈ ω 𝑥 ≈ 𝑧 → ∃𝑧 ∈ 𝑤 𝑥 ≈ 𝑧)) |
41 | 19, 40 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ∃𝑧 ∈ 𝑤 𝑥 ≈ 𝑧) |
42 | | r19.29 3282 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑧 ∈
𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ ∃𝑧 ∈ 𝑤 𝑥 ≈ 𝑧) → ∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧)) |
43 | 42 | expcom 404 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑧 ∈
𝑤 𝑥 ≈ 𝑧 → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → ∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧))) |
44 | 41, 43 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → ∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧))) |
45 | | ordom 7335 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ Ord
ω |
46 | | ordelss 5979 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Ord
ω ∧ 𝑤 ∈
ω) → 𝑤 ⊆
ω) |
47 | 45, 46 | mpan 681 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ω → 𝑤 ⊆
ω) |
48 | 47 | ad2antrr 717 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → 𝑤 ⊆ ω) |
49 | 48 | sseld 3826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (𝑧 ∈ 𝑤 → 𝑧 ∈ ω)) |
50 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ω → ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → (𝑥 ≈ 𝑧 → 𝜑))) |
51 | 50 | impd 400 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ω → (((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧) → 𝜑)) |
52 | 49, 51 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (𝑧 ∈ 𝑤 → (((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧) → 𝜑))) |
53 | 52 | rexlimdv 3239 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧) → 𝜑)) |
54 | 44, 53 | syld 47 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → 𝜑)) |
55 | 54 | ex 403 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (𝑥 ⊊ 𝑦 → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → 𝜑))) |
56 | 55 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → (𝑥 ⊊ 𝑦 → 𝜑))) |
57 | 56 | alimdv 2015 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑥∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → ∀𝑥(𝑥 ⊊ 𝑦 → 𝜑))) |
58 | 14, 57 | syl5bi 234 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → ∀𝑥(𝑥 ⊊ 𝑦 → 𝜑))) |
59 | | findcard3.3 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ Fin →
(∀𝑥(𝑥 ⊊ 𝑦 → 𝜑) → 𝜒)) |
60 | 10, 58, 59 | sylsyld 61 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → 𝜒)) |
61 | 60 | impancom 445 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ω ∧
∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) → (𝑦 ≈ 𝑤 → 𝜒)) |
62 | 61 | alrimiv 2026 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ω ∧
∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) → ∀𝑦(𝑦 ≈ 𝑤 → 𝜒)) |
63 | 62 | expcom 404 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → (𝑤 ∈ ω → ∀𝑦(𝑦 ≈ 𝑤 → 𝜒))) |
64 | | breq1 4876 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑤 ↔ 𝑦 ≈ 𝑤)) |
65 | | findcard3.1 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
66 | 64, 65 | imbi12d 336 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑦 ≈ 𝑤 → 𝜒))) |
67 | 66 | cbvalvw 2143 |
. . . . . . . . 9
⊢
(∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑦(𝑦 ≈ 𝑤 → 𝜒)) |
68 | 63, 67 | syl6ibr 244 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → (𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑))) |
69 | 68 | a1i 11 |
. . . . . . 7
⊢ (𝑤 ∈ On → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → (𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑)))) |
70 | 7, 69 | tfis2 7317 |
. . . . . 6
⊢ (𝑤 ∈ On → (𝑤 ∈ ω →
∀𝑥(𝑥 ≈ 𝑤 → 𝜑))) |
71 | 2, 70 | mpcom 38 |
. . . . 5
⊢ (𝑤 ∈ ω →
∀𝑥(𝑥 ≈ 𝑤 → 𝜑)) |
72 | 71 | rgen 3131 |
. . . 4
⊢
∀𝑤 ∈
ω ∀𝑥(𝑥 ≈ 𝑤 → 𝜑) |
73 | | r19.29 3282 |
. . . 4
⊢
((∀𝑤 ∈
ω ∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ ∃𝑤 ∈ ω 𝐴 ≈ 𝑤) → ∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤)) |
74 | 72, 73 | mpan 681 |
. . 3
⊢
(∃𝑤 ∈
ω 𝐴 ≈ 𝑤 → ∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤)) |
75 | 1, 74 | sylbi 209 |
. 2
⊢ (𝐴 ∈ Fin → ∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤)) |
76 | | breq1 4876 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ≈ 𝑤 ↔ 𝐴 ≈ 𝑤)) |
77 | | findcard3.2 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
78 | 76, 77 | imbi12d 336 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝐴 ≈ 𝑤 → 𝜏))) |
79 | 78 | spcgv 3510 |
. . . 4
⊢ (𝐴 ∈ Fin →
(∀𝑥(𝑥 ≈ 𝑤 → 𝜑) → (𝐴 ≈ 𝑤 → 𝜏))) |
80 | 79 | impd 400 |
. . 3
⊢ (𝐴 ∈ Fin →
((∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤) → 𝜏)) |
81 | 80 | rexlimdvw 3244 |
. 2
⊢ (𝐴 ∈ Fin → (∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤) → 𝜏)) |
82 | 75, 81 | mpd 15 |
1
⊢ (𝐴 ∈ Fin → 𝜏) |