| 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 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ∈ ω) |
| 21 | | nnfi 9207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 ∈ ω → 𝑧 ∈ Fin) |
| 22 | | ensymfib 9224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 ∈ Fin → (𝑧 ≈ 𝑥 ↔ 𝑥 ≈ 𝑧)) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 ∈ ω → (𝑧 ≈ 𝑥 ↔ 𝑥 ≈ 𝑧)) |
| 24 | 23 | biimpar 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → 𝑧 ≈ 𝑥) |
| 25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ≈ 𝑥) |
| 26 | | simplll 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑤 ∈ ω) |
| 27 | | php3 9249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ⊊ 𝑦) → 𝑥 ≺ 𝑦) |
| 28 | 10, 27 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → 𝑥 ≺ 𝑦) |
| 29 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑥 ≺ 𝑦) |
| 30 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑦 ≈ 𝑤) |
| 31 | | endom 9019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ≈ 𝑤 → 𝑦 ≼ 𝑤) |
| 32 | | nnfi 9207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑤 ∈ ω → 𝑤 ∈ Fin) |
| 33 | | domfi 9229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑤 ∈ Fin ∧ 𝑦 ≼ 𝑤) → 𝑦 ∈ Fin) |
| 34 | 32, 33 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≼ 𝑤) → 𝑦 ∈ Fin) |
| 35 | 34 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑤 ∈ ω ∧ 𝑥 ≺ 𝑦 ∧ 𝑦 ≼ 𝑤) → 𝑦 ∈ Fin) |
| 36 | | sdomdom 9020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ≺ 𝑦 → 𝑥 ≼ 𝑦) |
| 37 | | domfi 9229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ≼ 𝑦) → 𝑥 ∈ Fin) |
| 38 | 36, 37 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ≺ 𝑦) → 𝑥 ∈ Fin) |
| 39 | 38 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ≺ 𝑦 ∧ 𝑦 ≼ 𝑤) → 𝑥 ∈ Fin) |
| 40 | 35, 39 | syld3an1 1412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑤 ∈ ω ∧ 𝑥 ≺ 𝑦 ∧ 𝑦 ≼ 𝑤) → 𝑥 ∈ Fin) |
| 41 | | sdomdomtrfi 9241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ Fin ∧ 𝑥 ≺ 𝑦 ∧ 𝑦 ≼ 𝑤) → 𝑥 ≺ 𝑤) |
| 42 | 40, 41 | syld3an1 1412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑤 ∈ ω ∧ 𝑥 ≺ 𝑦 ∧ 𝑦 ≼ 𝑤) → 𝑥 ≺ 𝑤) |
| 43 | 31, 42 | syl3an3 1166 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑤 ∈ ω ∧ 𝑥 ≺ 𝑦 ∧ 𝑦 ≈ 𝑤) → 𝑥 ≺ 𝑤) |
| 44 | 26, 29, 30, 43 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑥 ≺ 𝑤) |
| 45 | | endom 9019 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ≈ 𝑥 → 𝑧 ≼ 𝑥) |
| 46 | | domsdomtrfi 9242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑧 ∈ Fin ∧ 𝑧 ≼ 𝑥 ∧ 𝑥 ≺ 𝑤) → 𝑧 ≺ 𝑤) |
| 47 | 21, 46 | syl3an1 1164 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ ω ∧ 𝑧 ≼ 𝑥 ∧ 𝑥 ≺ 𝑤) → 𝑧 ≺ 𝑤) |
| 48 | 45, 47 | syl3an2 1165 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ ω ∧ 𝑧 ≈ 𝑥 ∧ 𝑥 ≺ 𝑤) → 𝑧 ≺ 𝑤) |
| 49 | 20, 25, 44, 48 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ≺ 𝑤) |
| 50 | | nnsdomo 9270 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (𝑧 ≺ 𝑤 ↔ 𝑧 ⊊ 𝑤)) |
| 51 | | nnord 7895 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 ∈ ω → Ord 𝑧) |
| 52 | | nnord 7895 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ ω → Ord 𝑤) |
| 53 | | ordelpss 6412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Ord
𝑧 ∧ Ord 𝑤) → (𝑧 ∈ 𝑤 ↔ 𝑧 ⊊ 𝑤)) |
| 54 | 51, 52, 53 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (𝑧 ∈ 𝑤 ↔ 𝑧 ⊊ 𝑤)) |
| 55 | 50, 54 | bitr4d 282 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (𝑧 ≺ 𝑤 ↔ 𝑧 ∈ 𝑤)) |
| 56 | 20, 26, 55 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → (𝑧 ≺ 𝑤 ↔ 𝑧 ∈ 𝑤)) |
| 57 | 49, 56 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧)) → 𝑧 ∈ 𝑤) |
| 58 | 57 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → 𝑧 ∈ 𝑤)) |
| 59 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → 𝑥 ≈ 𝑧) |
| 60 | 58, 59 | jca2 513 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ((𝑧 ∈ ω ∧ 𝑥 ≈ 𝑧) → (𝑧 ∈ 𝑤 ∧ 𝑥 ≈ 𝑧))) |
| 61 | 60 | reximdv2 3164 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∃𝑧 ∈ ω 𝑥 ≈ 𝑧 → ∃𝑧 ∈ 𝑤 𝑥 ≈ 𝑧)) |
| 62 | 19, 61 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → ∃𝑧 ∈ 𝑤 𝑥 ≈ 𝑧) |
| 63 | | r19.29 3114 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑧 ∈
𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ ∃𝑧 ∈ 𝑤 𝑥 ≈ 𝑧) → ∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧)) |
| 64 | 63 | expcom 413 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑧 ∈
𝑤 𝑥 ≈ 𝑧 → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → ∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧))) |
| 65 | 62, 64 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → ∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧))) |
| 66 | | ordom 7897 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ Ord
ω |
| 67 | | ordelss 6400 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Ord
ω ∧ 𝑤 ∈
ω) → 𝑤 ⊆
ω) |
| 68 | 66, 67 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ω → 𝑤 ⊆
ω) |
| 69 | 68 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → 𝑤 ⊆ ω) |
| 70 | 69 | sseld 3982 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (𝑧 ∈ 𝑤 → 𝑧 ∈ ω)) |
| 71 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ω → ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → (𝑥 ≈ 𝑧 → 𝜑))) |
| 72 | 71 | impd 410 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ω → (((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧) → 𝜑)) |
| 73 | 70, 72 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (𝑧 ∈ 𝑤 → (((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧) → 𝜑))) |
| 74 | 73 | rexlimdv 3153 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∃𝑧 ∈ 𝑤 ((𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) ∧ 𝑥 ≈ 𝑧) → 𝜑)) |
| 75 | 65, 74 | syld 47 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) ∧ 𝑥 ⊊ 𝑦) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → 𝜑)) |
| 76 | 75 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (𝑥 ⊊ 𝑦 → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → 𝜑))) |
| 77 | 76 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → (𝑥 ⊊ 𝑦 → 𝜑))) |
| 78 | 77 | alimdv 1916 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑥∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → (𝑥 ≈ 𝑧 → 𝜑)) → ∀𝑥(𝑥 ⊊ 𝑦 → 𝜑))) |
| 79 | 14, 78 | biimtrid 242 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → ∀𝑥(𝑥 ⊊ 𝑦 → 𝜑))) |
| 80 | | findcard3.3 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ Fin →
(∀𝑥(𝑥 ⊊ 𝑦 → 𝜑) → 𝜒)) |
| 81 | 10, 79, 80 | sylsyld 61 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ω ∧ 𝑦 ≈ 𝑤) → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → 𝜒)) |
| 82 | 81 | impancom 451 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ω ∧
∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) → (𝑦 ≈ 𝑤 → 𝜒)) |
| 83 | 82 | alrimiv 1927 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ω ∧
∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑))) → ∀𝑦(𝑦 ≈ 𝑤 → 𝜒)) |
| 84 | 83 | expcom 413 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → (𝑤 ∈ ω → ∀𝑦(𝑦 ≈ 𝑤 → 𝜒))) |
| 85 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑤 ↔ 𝑦 ≈ 𝑤)) |
| 86 | | findcard3.1 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
| 87 | 85, 86 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑦 ≈ 𝑤 → 𝜒))) |
| 88 | 87 | cbvalvw 2035 |
. . . . . . . . 9
⊢
(∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑦(𝑦 ≈ 𝑤 → 𝜒)) |
| 89 | 84, 88 | imbitrrdi 252 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → (𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑))) |
| 90 | 89 | a1i 11 |
. . . . . . 7
⊢ (𝑤 ∈ On → (∀𝑧 ∈ 𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥 ≈ 𝑧 → 𝜑)) → (𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑)))) |
| 91 | 7, 90 | tfis2 7878 |
. . . . . 6
⊢ (𝑤 ∈ On → (𝑤 ∈ ω →
∀𝑥(𝑥 ≈ 𝑤 → 𝜑))) |
| 92 | 2, 91 | mpcom 38 |
. . . . 5
⊢ (𝑤 ∈ ω →
∀𝑥(𝑥 ≈ 𝑤 → 𝜑)) |
| 93 | 92 | rgen 3063 |
. . . 4
⊢
∀𝑤 ∈
ω ∀𝑥(𝑥 ≈ 𝑤 → 𝜑) |
| 94 | | r19.29 3114 |
. . . 4
⊢
((∀𝑤 ∈
ω ∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ ∃𝑤 ∈ ω 𝐴 ≈ 𝑤) → ∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤)) |
| 95 | 93, 94 | mpan 690 |
. . 3
⊢
(∃𝑤 ∈
ω 𝐴 ≈ 𝑤 → ∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤)) |
| 96 | 1, 95 | sylbi 217 |
. 2
⊢ (𝐴 ∈ Fin → ∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤)) |
| 97 | | breq1 5146 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ≈ 𝑤 ↔ 𝐴 ≈ 𝑤)) |
| 98 | | findcard3.2 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
| 99 | 97, 98 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝐴 ≈ 𝑤 → 𝜏))) |
| 100 | 99 | spcgv 3596 |
. . . 4
⊢ (𝐴 ∈ Fin →
(∀𝑥(𝑥 ≈ 𝑤 → 𝜑) → (𝐴 ≈ 𝑤 → 𝜏))) |
| 101 | 100 | impd 410 |
. . 3
⊢ (𝐴 ∈ Fin →
((∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤) → 𝜏)) |
| 102 | 101 | rexlimdvw 3160 |
. 2
⊢ (𝐴 ∈ Fin → (∃𝑤 ∈ ω (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ∧ 𝐴 ≈ 𝑤) → 𝜏)) |
| 103 | 96, 102 | mpd 15 |
1
⊢ (𝐴 ∈ Fin → 𝜏) |