| Step | Hyp | Ref
| Expression |
| 1 | | isfi 9016 |
. . 3
⊢ (𝐴 ∈ Fin ↔ ∃𝑤 ∈ ω 𝐴 ≈ 𝑤) |
| 2 | | nnon 7893 |
. . . . . 6
⊢ (𝑤 ∈ ω → 𝑤 ∈ On) |
| 3 | | eleq1w 2824 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (𝑤 ∈ ω ↔ 𝑧 ∈ ω)) |
| 4 | | breq2 5147 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ 𝑧)) |
| 5 | 4 | imbi1d 341 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ 𝑧 → 𝜑))) |
| 6 | 5 | albidv 1920 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) |
| 7 | 3, 6 | imbi12d 344 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → ((𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑)) ↔ (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)))) |
| 8 | | rspe 3249 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → ∃𝑤 ∈ ω 𝑦 ≈ 𝑤) |
| 9 | | isfi 9016 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑦 ≈ 𝑤) |
| 10 | 8, 9 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → 𝑦 ∈ Fin) |
| 11 | | 19.21v 1939 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥(𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ↔ (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) |
| 12 | 11 | ralbii 3093 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝑤 ∀𝑥(𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ↔ ∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) |
| 13 | | ralcom4 3286 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝑤 ∀𝑥(𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ↔ ∀𝑥∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑))) |
| 14 | 12, 13 | bitr3i 277 |
. . . . . . . . . . . . . 14
⊢
(∀𝑧 ∈
𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) ↔ ∀𝑥∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑))) |
| 15 | | pssss 4098 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ⊊ 𝑦 → 𝑥 ⊆ 𝑦) |
| 16 | | ssfi 9213 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ⊆ 𝑦) → 𝑥 ∈ Fin) |
| 17 | | isfi 9016 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ Fin ↔ ∃𝑧 ∈ ω 𝑥 ≈ 𝑧) |
| 18 | 16, 17 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ⊆ 𝑦) → ∃𝑧 ∈ ω 𝑥 ≈ 𝑧) |
| 19 | 10, 15, 18 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ∃𝑧 ∈ ω 𝑥 ≈ 𝑧) |
| 20 | | ensym 9043 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ≈ 𝑧 → 𝑧 ≈ 𝑥) |
| 21 | 20 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ≈ 𝑥) |
| 22 | | php3 9249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ⊊ 𝑦) → 𝑥 ≺ 𝑦) |
| 23 | 10, 22 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → 𝑥 ≺ 𝑦) |
| 24 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑦 ≈ 𝑤) |
| 25 | | sdomentr 9151 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ≺ 𝑦 ∧ 𝑦 ≈ 𝑤) → 𝑥 ≺ 𝑤) |
| 26 | 23, 24, 25 | syl2an2r 685 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑥 ≺ 𝑤) |
| 27 | | ensdomtr 9153 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ≈ 𝑥 ∧ 𝑥 ≺ 𝑤) → 𝑧 ≺ 𝑤) |
| 28 | 21, 26, 27 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ≺ 𝑤) |
| 29 | | nnon 7893 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ω → 𝑧 ∈ On) |
| 30 | 29 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ∈ On) |
| 31 | 2 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑤 ∈ On) |
| 32 | | sdomel 9164 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ≺ 𝑤 → 𝑧 ∈ 𝑤)) |
| 33 | 30, 31, 32 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → (𝑧 ≺ 𝑤 → 𝑧 ∈ 𝑤)) |
| 34 | 28, 33 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ∈ 𝑤) |
| 35 | 34 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → 𝑧 ∈ 𝑤)) |
| 36 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → 𝑥 ≈ 𝑧) |
| 37 | 35, 36 | jca2 513 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → (𝑧 ∈ 𝑤 ∧ 𝑥 ≈ 𝑧))) |
| 38 | 37 | reximdv2 3164 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∃𝑧 ∈ ω 𝑥 ≈ 𝑧 → ∃𝑧 ∈ 𝑤 𝑥 ≈ 𝑧)) |
| 39 | 19, 38 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ∃𝑧 ∈ 𝑤 𝑥 ≈ 𝑧) |
| 40 | | r19.29 3114 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑧 ∈
𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ ∃𝑧 ∈ 𝑤 𝑥 ≈ 𝑧) → ∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧)) |
| 41 | 40 | expcom 413 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑧 ∈
𝑤 𝑥 ≈ 𝑧 → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → ∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧))) |
| 42 | 39, 41 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → ∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧))) |
| 43 | | ordom 7897 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ Ord
ω |
| 44 | | ordelss 6400 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Ord
ω ∧ 𝑤 ∈
ω) → 𝑤 ⊆
ω) |
| 45 | 43, 44 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ω → 𝑤 ⊆
ω) |
| 46 | 45 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → 𝑤 ⊆ ω) |
| 47 | 46 | sseld 3982 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (𝑧 ∈ 𝑤 → 𝑧 ∈ ω)) |
| 48 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ω → ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → (𝑥 ≈ 𝑧 → 𝜑))) |
| 49 | 48 | impd 410 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ω → (((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧) → 𝜑)) |
| 50 | 47, 49 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (𝑧 ∈ 𝑤 → (((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧) → 𝜑))) |
| 51 | 50 | rexlimdv 3153 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧) → 𝜑)) |
| 52 | 42, 51 | syld 47 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → 𝜑)) |
| 53 | 52 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (𝑥 ⊊ 𝑦 → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → 𝜑))) |
| 54 | 53 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → (𝑥 ⊊ 𝑦 → 𝜑))) |
| 55 | 54 | alimdv 1916 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑥∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → ∀𝑥(𝑥 ⊊ 𝑦 → 𝜑))) |
| 56 | 14, 55 | biimtrid 242 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → ∀𝑥(𝑥 ⊊ 𝑦 → 𝜑))) |
| 57 | | findcard3OLD.3 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ Fin →
(∀𝑥(𝑥 ⊊ 𝑦 → 𝜑) → 𝜒)) |
| 58 | 10, 56, 57 | sylsyld 61 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → 𝜒)) |
| 59 | 58 | impancom 451 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ω ∧
∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) → (𝑦 ≈ 𝑤 → 𝜒)) |
| 60 | 59 | alrimiv 1927 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ω ∧
∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) → ∀𝑦(𝑦 ≈ 𝑤 → 𝜒)) |
| 61 | 60 | expcom 413 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → (𝑤 ∈ ω → ∀𝑦(𝑦 ≈ 𝑤 → 𝜒))) |
| 62 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑤 ↔ 𝑦 ≈ 𝑤)) |
| 63 | | findcard3OLD.1 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
| 64 | 62, 63 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑦 ≈ 𝑤 → 𝜒))) |
| 65 | 64 | cbvalvw 2035 |
. . . . . . . . 9
⊢
(∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑦(𝑦 ≈ 𝑤 → 𝜒)) |
| 66 | 61, 65 | imbitrrdi 252 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → (𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑))) |
| 67 | 66 | a1i 11 |
. . . . . . 7
⊢ (𝑤 ∈ On → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → (𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑)))) |
| 68 | 7, 67 | tfis2 7878 |
. . . . . 6
⊢ (𝑤 ∈ On → (𝑤 ∈ ω →
∀𝑥(𝑥 ≈ 𝑤 → 𝜑))) |
| 69 | 2, 68 | mpcom 38 |
. . . . 5
⊢ (𝑤 ∈ ω →
∀𝑥(𝑥 ≈ 𝑤 → 𝜑)) |
| 70 | 69 | rgen 3063 |
. . . 4
⊢
∀𝑤 ∈
ω ∀𝑥(𝑥 ≈ 𝑤 → 𝜑) |
| 71 | | r19.29 3114 |
. . . 4
⊢
((∀𝑤 ∈
ω ∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ ∃𝑤 ∈ ω 𝐴 ≈ 𝑤) → ∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤)) |
| 72 | 70, 71 | mpan 690 |
. . 3
⊢
(∃𝑤 ∈
ω 𝐴 ≈ 𝑤 → ∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤)) |
| 73 | 1, 72 | sylbi 217 |
. 2
⊢ (𝐴 ∈ Fin → ∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤)) |
| 74 | | breq1 5146 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ≈ 𝑤 ↔ 𝐴 ≈ 𝑤)) |
| 75 | | findcard3OLD.2 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
| 76 | 74, 75 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝐴 ≈ 𝑤 → 𝜏))) |
| 77 | 76 | spcgv 3596 |
. . . 4
⊢ (𝐴 ∈ Fin →
(∀𝑥(𝑥 ≈ 𝑤 → 𝜑) → (𝐴 ≈ 𝑤 → 𝜏))) |
| 78 | 77 | impd 410 |
. . 3
⊢ (𝐴 ∈ Fin →
((∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤) → 𝜏)) |
| 79 | 78 | rexlimdvw 3160 |
. 2
⊢ (𝐴 ∈ Fin → (∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤) → 𝜏)) |
| 80 | 73, 79 | mpd 15 |
1
⊢ (𝐴 ∈ Fin → 𝜏) |