Step | Hyp | Ref
| Expression |
1 | | findcard2s.4 |
. 2
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
2 | | isfi 6739 |
. . 3
⊢ (𝑥 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑥 ≈ 𝑤) |
3 | | breq2 3993 |
. . . . . . . 8
⊢ (𝑤 = ∅ → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ ∅)) |
4 | 3 | imbi1d 230 |
. . . . . . 7
⊢ (𝑤 = ∅ → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ ∅ → 𝜑))) |
5 | 4 | albidv 1817 |
. . . . . 6
⊢ (𝑤 = ∅ → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ ∅ → 𝜑))) |
6 | | breq2 3993 |
. . . . . . . 8
⊢ (𝑤 = 𝑣 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ 𝑣)) |
7 | 6 | imbi1d 230 |
. . . . . . 7
⊢ (𝑤 = 𝑣 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ 𝑣 → 𝜑))) |
8 | 7 | albidv 1817 |
. . . . . 6
⊢ (𝑤 = 𝑣 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ 𝑣 → 𝜑))) |
9 | | breq2 3993 |
. . . . . . . 8
⊢ (𝑤 = suc 𝑣 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ suc 𝑣)) |
10 | 9 | imbi1d 230 |
. . . . . . 7
⊢ (𝑤 = suc 𝑣 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ suc 𝑣 → 𝜑))) |
11 | 10 | albidv 1817 |
. . . . . 6
⊢ (𝑤 = suc 𝑣 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑))) |
12 | | en0 6773 |
. . . . . . . 8
⊢ (𝑥 ≈ ∅ ↔ 𝑥 = ∅) |
13 | | findcard2s.5 |
. . . . . . . . 9
⊢ 𝜓 |
14 | | findcard2s.1 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) |
15 | 13, 14 | mpbiri 167 |
. . . . . . . 8
⊢ (𝑥 = ∅ → 𝜑) |
16 | 12, 15 | sylbi 120 |
. . . . . . 7
⊢ (𝑥 ≈ ∅ → 𝜑) |
17 | 16 | ax-gen 1442 |
. . . . . 6
⊢
∀𝑥(𝑥 ≈ ∅ → 𝜑) |
18 | | peano3 4580 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ω → suc 𝑣 ≠ ∅) |
19 | 18 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 ≠ ∅) |
20 | | breq1 3992 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = ∅ → (𝑤 ≈ suc 𝑣 ↔ ∅ ≈ suc 𝑣)) |
21 | 20 | anbi2d 461 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ↔ (𝑣 ∈ ω ∧ ∅ ≈ suc
𝑣))) |
22 | | peano1 4578 |
. . . . . . . . . . . . . . . . . 18
⊢ ∅
∈ ω |
23 | | peano2 4579 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ ω → suc 𝑣 ∈
ω) |
24 | | nneneq 6835 |
. . . . . . . . . . . . . . . . . 18
⊢ ((∅
∈ ω ∧ suc 𝑣
∈ ω) → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣)) |
25 | 22, 23, 24 | sylancr 412 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ ω → (∅
≈ suc 𝑣 ↔
∅ = suc 𝑣)) |
26 | 25 | biimpa 294 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ ω ∧ ∅
≈ suc 𝑣) →
∅ = suc 𝑣) |
27 | 26 | eqcomd 2176 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ ω ∧ ∅
≈ suc 𝑣) → suc
𝑣 =
∅) |
28 | 21, 27 | syl6bi 162 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 = ∅)) |
29 | 28 | com12 30 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 = ∅ → suc 𝑣 = ∅)) |
30 | 29 | necon3d 2384 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (suc 𝑣 ≠ ∅ → 𝑤 ≠ ∅)) |
31 | 19, 30 | mpd 13 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ≠ ∅) |
32 | 31 | ex 114 |
. . . . . . . . . 10
⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → 𝑤 ≠ ∅)) |
33 | | nnfi 6850 |
. . . . . . . . . . . . . . . 16
⊢ (suc
𝑣 ∈ ω → suc
𝑣 ∈
Fin) |
34 | 23, 33 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ ω → suc 𝑣 ∈ Fin) |
35 | 34 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 ∈ Fin) |
36 | | enfi 6851 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ≈ suc 𝑣 → (𝑤 ∈ Fin ↔ suc 𝑣 ∈ Fin)) |
37 | 36 | adantl 275 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ∈ Fin ↔ suc 𝑣 ∈ Fin)) |
38 | 35, 37 | mpbird 166 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ∈ Fin) |
39 | | fin0 6863 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ Fin → (𝑤 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝑤)) |
40 | 38, 39 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝑤)) |
41 | | simpll 524 |
. . . . . . . . . . . . . . 15
⊢ (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧 ∈ 𝑤) → 𝑣 ∈ ω) |
42 | | dif1en 6857 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ∧ 𝑧 ∈ 𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣) |
43 | 42 | 3expa 1198 |
. . . . . . . . . . . . . . 15
⊢ (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧 ∈ 𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣) |
44 | | fidifsnid 6849 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ Fin ∧ 𝑧 ∈ 𝑤) → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤) |
45 | 38, 44 | sylan 281 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧 ∈ 𝑤) → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤) |
46 | | neldifsn 3713 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬
𝑧 ∈ (𝑤 ∖ {𝑧}) |
47 | | vex 2733 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑤 ∈ V |
48 | | difexg 4130 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ V → (𝑤 ∖ {𝑧}) ∈ V) |
49 | 47, 48 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∖ {𝑧}) ∈ V |
50 | | breq1 3992 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ≈ 𝑣 ↔ (𝑤 ∖ {𝑧}) ≈ 𝑣)) |
51 | 50 | anbi2d 461 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ↔ (𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣))) |
52 | | eleq2 2234 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ (𝑤 ∖ {𝑧}))) |
53 | 52 | notbid 662 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (¬ 𝑧 ∈ 𝑦 ↔ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧}))) |
54 | 51, 53 | anbi12d 470 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ∧ ¬ 𝑧 ∈ 𝑦) ↔ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) ∧ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})))) |
55 | | uneq1 3274 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ∪ {𝑧}) = ((𝑤 ∖ {𝑧}) ∪ {𝑧})) |
56 | 55 | sbceq1d 2960 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑 ↔ [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)) |
57 | 56 | imbi2d 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ((∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))) |
58 | 54, 57 | imbi12d 233 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ((((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑)) ↔ (((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) ∧ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)))) |
59 | | breq1 3992 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑣 ↔ 𝑦 ≈ 𝑣)) |
60 | | findcard2s.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
61 | 59, 60 | imbi12d 233 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑣 → 𝜑) ↔ (𝑦 ≈ 𝑣 → 𝜒))) |
62 | 61 | spv 1853 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → (𝑦 ≈ 𝑣 → 𝜒)) |
63 | | pm2.27 40 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ≈ 𝑣 → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜒)) |
64 | 63 | adantl 275 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜒)) |
65 | 64 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜒)) |
66 | | rspe 2519 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ∃𝑣 ∈ ω 𝑦 ≈ 𝑣) |
67 | | isfi 6739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ Fin ↔ ∃𝑣 ∈ ω 𝑦 ≈ 𝑣) |
68 | 66, 67 | sylibr 133 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → 𝑦 ∈ Fin) |
69 | | findcard2s.6 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝜒 → 𝜃)) |
70 | 68, 69 | sylan 281 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ∧ ¬ 𝑧 ∈ 𝑦) → (𝜒 → 𝜃)) |
71 | 65, 70 | syld 45 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜃)) |
72 | 62, 71 | syl5 32 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → 𝜃)) |
73 | | vex 2733 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑦 ∈ V |
74 | | vex 2733 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑧 ∈ V |
75 | 74 | snex 4171 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ {𝑧} ∈ V |
76 | 73, 75 | unex 4426 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∪ {𝑧}) ∈ V |
77 | | findcard2s.3 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃)) |
78 | 76, 77 | sbcie 2989 |
. . . . . . . . . . . . . . . . . . . 20
⊢
([(𝑦 ∪
{𝑧}) / 𝑥]𝜑 ↔ 𝜃) |
79 | 72, 78 | syl6ibr 161 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑)) |
80 | 49, 58, 79 | vtocl 2784 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) ∧ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)) |
81 | 46, 80 | mpan2 423 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)) |
82 | | dfsbcq 2957 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ([((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑 ↔ [𝑤 / 𝑥]𝜑)) |
83 | 82 | imbi2d 229 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))) |
84 | 81, 83 | syl5ib 153 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))) |
85 | 45, 84 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧 ∈ 𝑤) → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))) |
86 | 41, 43, 85 | mp2and 431 |
. . . . . . . . . . . . . 14
⊢ (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧 ∈ 𝑤) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)) |
87 | 86 | ex 114 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧 ∈ 𝑤 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))) |
88 | 87 | exlimdv 1812 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (∃𝑧 𝑧 ∈ 𝑤 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))) |
89 | 40, 88 | sylbid 149 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))) |
90 | 89 | ex 114 |
. . . . . . . . . 10
⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (𝑤 ≠ ∅ → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))) |
91 | 32, 90 | mpdd 41 |
. . . . . . . . 9
⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))) |
92 | 91 | com23 78 |
. . . . . . . 8
⊢ (𝑣 ∈ ω →
(∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → (𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑))) |
93 | 92 | alrimdv 1869 |
. . . . . . 7
⊢ (𝑣 ∈ ω →
(∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → ∀𝑤(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑))) |
94 | | nfv 1521 |
. . . . . . . 8
⊢
Ⅎ𝑤(𝑥 ≈ suc 𝑣 → 𝜑) |
95 | | nfv 1521 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑤 ≈ suc 𝑣 |
96 | | nfsbc1v 2973 |
. . . . . . . . 9
⊢
Ⅎ𝑥[𝑤 / 𝑥]𝜑 |
97 | 95, 96 | nfim 1565 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑) |
98 | | breq1 3992 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → (𝑥 ≈ suc 𝑣 ↔ 𝑤 ≈ suc 𝑣)) |
99 | | sbceq1a 2964 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑥]𝜑)) |
100 | 98, 99 | imbi12d 233 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → ((𝑥 ≈ suc 𝑣 → 𝜑) ↔ (𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑))) |
101 | 94, 97, 100 | cbval 1747 |
. . . . . . 7
⊢
(∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑) ↔ ∀𝑤(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)) |
102 | 93, 101 | syl6ibr 161 |
. . . . . 6
⊢ (𝑣 ∈ ω →
(∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → ∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑))) |
103 | 5, 8, 11, 17, 102 | finds1 4586 |
. . . . 5
⊢ (𝑤 ∈ ω →
∀𝑥(𝑥 ≈ 𝑤 → 𝜑)) |
104 | 103 | 19.21bi 1551 |
. . . 4
⊢ (𝑤 ∈ ω → (𝑥 ≈ 𝑤 → 𝜑)) |
105 | 104 | rexlimiv 2581 |
. . 3
⊢
(∃𝑤 ∈
ω 𝑥 ≈ 𝑤 → 𝜑) |
106 | 2, 105 | sylbi 120 |
. 2
⊢ (𝑥 ∈ Fin → 𝜑) |
107 | 1, 106 | vtoclga 2796 |
1
⊢ (𝐴 ∈ Fin → 𝜏) |