| Step | Hyp | Ref
| Expression |
| 1 | | eleq1w 2824 |
. . . . . 6
⊢ (𝑐 = 𝑎 → (𝑐 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴)) |
| 2 | 1 | anbi2d 630 |
. . . . 5
⊢ (𝑐 = 𝑎 → ((𝜂 ∧ 𝑐 ∈ 𝐴) ↔ (𝜂 ∧ 𝑎 ∈ 𝐴))) |
| 3 | | sbceq2a 3800 |
. . . . 5
⊢ (𝑐 = 𝑎 → ([𝑐 / 𝑎]𝜁 ↔ 𝜁)) |
| 4 | 2, 3 | anbi12d 632 |
. . . 4
⊢ (𝑐 = 𝑎 → (((𝜂 ∧ 𝑐 ∈ 𝐴) ∧ [𝑐 / 𝑎]𝜁) ↔ ((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ 𝜁))) |
| 5 | 4 | imbi1d 341 |
. . 3
⊢ (𝑐 = 𝑎 → ((((𝜂 ∧ 𝑐 ∈ 𝐴) ∧ [𝑐 / 𝑎]𝜁) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ (𝜎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) ↔ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ 𝜁) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ (𝜎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))) |
| 6 | | fdc1.1 |
. . . . . 6
⊢ 𝐴 ∈ V |
| 7 | | fdc1.2 |
. . . . . 6
⊢ 𝑀 ∈ ℤ |
| 8 | | fdc1.3 |
. . . . . 6
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 9 | | fdc1.4 |
. . . . . 6
⊢ 𝑁 = (𝑀 + 1) |
| 10 | | sbsbc 3792 |
. . . . . . 7
⊢ ([𝑑 / 𝑎]𝜑 ↔ [𝑑 / 𝑎]𝜑) |
| 11 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑎𝜓 |
| 12 | | fdc1.6 |
. . . . . . . 8
⊢ (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑 ↔ 𝜓)) |
| 13 | 11, 12 | sbhypf 3544 |
. . . . . . 7
⊢ (𝑑 = (𝑓‘(𝑘 − 1)) → ([𝑑 / 𝑎]𝜑 ↔ 𝜓)) |
| 14 | 10, 13 | bitr3id 285 |
. . . . . 6
⊢ (𝑑 = (𝑓‘(𝑘 − 1)) → ([𝑑 / 𝑎]𝜑 ↔ 𝜓)) |
| 15 | | fdc1.7 |
. . . . . 6
⊢ (𝑏 = (𝑓‘𝑘) → (𝜓 ↔ 𝜒)) |
| 16 | | sbsbc 3792 |
. . . . . . 7
⊢ ([𝑑 / 𝑎]𝜃 ↔ [𝑑 / 𝑎]𝜃) |
| 17 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑎𝜏 |
| 18 | | fdc1.8 |
. . . . . . . 8
⊢ (𝑎 = (𝑓‘𝑛) → (𝜃 ↔ 𝜏)) |
| 19 | 17, 18 | sbhypf 3544 |
. . . . . . 7
⊢ (𝑑 = (𝑓‘𝑛) → ([𝑑 / 𝑎]𝜃 ↔ 𝜏)) |
| 20 | 16, 19 | bitr3id 285 |
. . . . . 6
⊢ (𝑑 = (𝑓‘𝑛) → ([𝑑 / 𝑎]𝜃 ↔ 𝜏)) |
| 21 | | simprl 771 |
. . . . . 6
⊢ ((𝜂 ∧ (𝑐 ∈ 𝐴 ∧ [𝑐 / 𝑎]𝜁)) → 𝑐 ∈ 𝐴) |
| 22 | | fdc1.10 |
. . . . . . 7
⊢ (𝜂 → 𝑅 Fr 𝐴) |
| 23 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜂 ∧ (𝑐 ∈ 𝐴 ∧ [𝑐 / 𝑎]𝜁)) → 𝑅 Fr 𝐴) |
| 24 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑎(𝜂 ∧ 𝑑 ∈ 𝐴) |
| 25 | | nfsbc1v 3808 |
. . . . . . . . . 10
⊢
Ⅎ𝑎[𝑑 / 𝑎]𝜃 |
| 26 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑎𝐴 |
| 27 | | nfsbc1v 3808 |
. . . . . . . . . . 11
⊢
Ⅎ𝑎[𝑑 / 𝑎]𝜑 |
| 28 | 26, 27 | nfrexw 3313 |
. . . . . . . . . 10
⊢
Ⅎ𝑎∃𝑏 ∈ 𝐴 [𝑑 / 𝑎]𝜑 |
| 29 | 25, 28 | nfor 1904 |
. . . . . . . . 9
⊢
Ⅎ𝑎([𝑑 / 𝑎]𝜃 ∨ ∃𝑏 ∈ 𝐴 [𝑑 / 𝑎]𝜑) |
| 30 | 24, 29 | nfim 1896 |
. . . . . . . 8
⊢
Ⅎ𝑎((𝜂 ∧ 𝑑 ∈ 𝐴) → ([𝑑 / 𝑎]𝜃 ∨ ∃𝑏 ∈ 𝐴 [𝑑 / 𝑎]𝜑)) |
| 31 | | eleq1w 2824 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑑 → (𝑎 ∈ 𝐴 ↔ 𝑑 ∈ 𝐴)) |
| 32 | 31 | anbi2d 630 |
. . . . . . . . 9
⊢ (𝑎 = 𝑑 → ((𝜂 ∧ 𝑎 ∈ 𝐴) ↔ (𝜂 ∧ 𝑑 ∈ 𝐴))) |
| 33 | | sbceq1a 3799 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑑 → (𝜃 ↔ [𝑑 / 𝑎]𝜃)) |
| 34 | | sbceq1a 3799 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑑 → (𝜑 ↔ [𝑑 / 𝑎]𝜑)) |
| 35 | 34 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑑 → (∃𝑏 ∈ 𝐴 𝜑 ↔ ∃𝑏 ∈ 𝐴 [𝑑 / 𝑎]𝜑)) |
| 36 | 33, 35 | orbi12d 919 |
. . . . . . . . 9
⊢ (𝑎 = 𝑑 → ((𝜃 ∨ ∃𝑏 ∈ 𝐴 𝜑) ↔ ([𝑑 / 𝑎]𝜃 ∨ ∃𝑏 ∈ 𝐴 [𝑑 / 𝑎]𝜑))) |
| 37 | 32, 36 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑎 = 𝑑 → (((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝜃 ∨ ∃𝑏 ∈ 𝐴 𝜑)) ↔ ((𝜂 ∧ 𝑑 ∈ 𝐴) → ([𝑑 / 𝑎]𝜃 ∨ ∃𝑏 ∈ 𝐴 [𝑑 / 𝑎]𝜑)))) |
| 38 | | fdc1.11 |
. . . . . . . 8
⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝜃 ∨ ∃𝑏 ∈ 𝐴 𝜑)) |
| 39 | 30, 37, 38 | chvarfv 2240 |
. . . . . . 7
⊢ ((𝜂 ∧ 𝑑 ∈ 𝐴) → ([𝑑 / 𝑎]𝜃 ∨ ∃𝑏 ∈ 𝐴 [𝑑 / 𝑎]𝜑)) |
| 40 | 39 | adantlr 715 |
. . . . . 6
⊢ (((𝜂 ∧ (𝑐 ∈ 𝐴 ∧ [𝑐 / 𝑎]𝜁)) ∧ 𝑑 ∈ 𝐴) → ([𝑑 / 𝑎]𝜃 ∨ ∃𝑏 ∈ 𝐴 [𝑑 / 𝑎]𝜑)) |
| 41 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑎𝜂 |
| 42 | 41, 27 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑎(𝜂 ∧ [𝑑 / 𝑎]𝜑) |
| 43 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑎(𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) |
| 44 | 42, 43 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑎((𝜂 ∧ [𝑑 / 𝑎]𝜑) ∧ (𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) |
| 45 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑎 𝑏𝑅𝑑 |
| 46 | 44, 45 | nfim 1896 |
. . . . . . . 8
⊢
Ⅎ𝑎(((𝜂 ∧ [𝑑 / 𝑎]𝜑) ∧ (𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑑) |
| 47 | 34 | anbi2d 630 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑑 → ((𝜂 ∧ 𝜑) ↔ (𝜂 ∧ [𝑑 / 𝑎]𝜑))) |
| 48 | 31 | anbi1d 631 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑑 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ↔ (𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) |
| 49 | 47, 48 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑎 = 𝑑 → (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ↔ ((𝜂 ∧ [𝑑 / 𝑎]𝜑) ∧ (𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)))) |
| 50 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑎 = 𝑑 → (𝑏𝑅𝑎 ↔ 𝑏𝑅𝑑)) |
| 51 | 49, 50 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑎 = 𝑑 → ((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑎) ↔ (((𝜂 ∧ [𝑑 / 𝑎]𝜑) ∧ (𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑑))) |
| 52 | | fdc1.12 |
. . . . . . . 8
⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑎) |
| 53 | 46, 51, 52 | chvarfv 2240 |
. . . . . . 7
⊢ (((𝜂 ∧ [𝑑 / 𝑎]𝜑) ∧ (𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑑) |
| 54 | 53 | adantllr 719 |
. . . . . 6
⊢ ((((𝜂 ∧ (𝑐 ∈ 𝐴 ∧ [𝑐 / 𝑎]𝜁)) ∧ [𝑑 / 𝑎]𝜑) ∧ (𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑑) |
| 55 | 6, 7, 8, 9, 14, 15, 20, 21, 23, 40, 54 | fdc 37752 |
. . . . 5
⊢ ((𝜂 ∧ (𝑐 ∈ 𝐴 ∧ [𝑐 / 𝑎]𝜁)) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) |
| 56 | 55 | anassrs 467 |
. . . 4
⊢ (((𝜂 ∧ 𝑐 ∈ 𝐴) ∧ [𝑐 / 𝑎]𝜁) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) |
| 57 | | idd 24 |
. . . . . . 7
⊢ (((𝜂 ∧ 𝑐 ∈ 𝐴) ∧ [𝑐 / 𝑎]𝜁) → (𝑓:(𝑀...𝑛)⟶𝐴 → 𝑓:(𝑀...𝑛)⟶𝐴)) |
| 58 | | dfsbcq 3790 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑀) = 𝑐 → ([(𝑓‘𝑀) / 𝑎]𝜁 ↔ [𝑐 / 𝑎]𝜁)) |
| 59 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝑓‘𝑀) ∈ V |
| 60 | | fdc1.5 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑓‘𝑀) → (𝜁 ↔ 𝜎)) |
| 61 | 59, 60 | sbcie 3830 |
. . . . . . . . . . 11
⊢
([(𝑓‘𝑀) / 𝑎]𝜁 ↔ 𝜎) |
| 62 | 58, 61 | bitr3di 286 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑀) = 𝑐 → ([𝑐 / 𝑎]𝜁 ↔ 𝜎)) |
| 63 | 62 | biimpcd 249 |
. . . . . . . . 9
⊢
([𝑐 / 𝑎]𝜁 → ((𝑓‘𝑀) = 𝑐 → 𝜎)) |
| 64 | 63 | adantl 481 |
. . . . . . . 8
⊢ (((𝜂 ∧ 𝑐 ∈ 𝐴) ∧ [𝑐 / 𝑎]𝜁) → ((𝑓‘𝑀) = 𝑐 → 𝜎)) |
| 65 | 64 | anim1d 611 |
. . . . . . 7
⊢ (((𝜂 ∧ 𝑐 ∈ 𝐴) ∧ [𝑐 / 𝑎]𝜁) → (((𝑓‘𝑀) = 𝑐 ∧ 𝜏) → (𝜎 ∧ 𝜏))) |
| 66 | | idd 24 |
. . . . . . 7
⊢ (((𝜂 ∧ 𝑐 ∈ 𝐴) ∧ [𝑐 / 𝑎]𝜁) → (∀𝑘 ∈ (𝑁...𝑛)𝜒 → ∀𝑘 ∈ (𝑁...𝑛)𝜒)) |
| 67 | 57, 65, 66 | 3anim123d 1445 |
. . . . . 6
⊢ (((𝜂 ∧ 𝑐 ∈ 𝐴) ∧ [𝑐 / 𝑎]𝜁) → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) → (𝑓:(𝑀...𝑛)⟶𝐴 ∧ (𝜎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
| 68 | 67 | eximdv 1917 |
. . . . 5
⊢ (((𝜂 ∧ 𝑐 ∈ 𝐴) ∧ [𝑐 / 𝑎]𝜁) → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) → ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ (𝜎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
| 69 | 68 | reximdv 3170 |
. . . 4
⊢ (((𝜂 ∧ 𝑐 ∈ 𝐴) ∧ [𝑐 / 𝑎]𝜁) → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ (𝜎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
| 70 | 56, 69 | mpd 15 |
. . 3
⊢ (((𝜂 ∧ 𝑐 ∈ 𝐴) ∧ [𝑐 / 𝑎]𝜁) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ (𝜎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) |
| 71 | 5, 70 | chvarvv 1998 |
. 2
⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ 𝜁) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ (𝜎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) |
| 72 | | fdc1.9 |
. 2
⊢ (𝜂 → ∃𝑎 ∈ 𝐴 𝜁) |
| 73 | 71, 72 | r19.29a 3162 |
1
⊢ (𝜂 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ (𝜎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) |