Step | Hyp | Ref
| Expression |
1 | | tfinds.2 |
. 2
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
2 | | tfinds.4 |
. 2
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
3 | | dflim3 7626 |
. . . . 5
⊢ (Lim
𝑥 ↔ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦))) |
4 | 3 | notbii 323 |
. . . 4
⊢ (¬
Lim 𝑥 ↔ ¬ (Ord
𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦))) |
5 | | iman 405 |
. . . . 5
⊢ ((Ord
𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) ↔ ¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦))) |
6 | | eloni 6223 |
. . . . . . 7
⊢ (𝑥 ∈ On → Ord 𝑥) |
7 | | pm2.27 42 |
. . . . . . 7
⊢ (Ord
𝑥 → ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦))) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ On → ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦))) |
9 | | tfinds.5 |
. . . . . . . . 9
⊢ 𝜓 |
10 | | tfinds.1 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) |
11 | 9, 10 | mpbiri 261 |
. . . . . . . 8
⊢ (𝑥 = ∅ → 𝜑) |
12 | 11 | a1d 25 |
. . . . . . 7
⊢ (𝑥 = ∅ → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)) |
13 | | nfra1 3140 |
. . . . . . . . 9
⊢
Ⅎ𝑦∀𝑦 ∈ 𝑥 𝜒 |
14 | | nfv 1922 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝜑 |
15 | 13, 14 | nfim 1904 |
. . . . . . . 8
⊢
Ⅎ𝑦(∀𝑦 ∈ 𝑥 𝜒 → 𝜑) |
16 | | vex 3412 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
17 | 16 | sucid 6292 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ suc 𝑦 |
18 | 1 | rspcv 3532 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ suc 𝑦 → (∀𝑥 ∈ suc 𝑦𝜑 → 𝜒)) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
suc 𝑦𝜑 → 𝜒) |
20 | | tfinds.6 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ On → (𝜒 → 𝜃)) |
21 | 19, 20 | syl5 34 |
. . . . . . . . . 10
⊢ (𝑦 ∈ On → (∀𝑥 ∈ suc 𝑦𝜑 → 𝜃)) |
22 | | raleq 3319 |
. . . . . . . . . . . 12
⊢ (𝑥 = suc 𝑦 → (∀𝑧 ∈ 𝑥 [𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑)) |
23 | | nfv 1922 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥𝜒 |
24 | 23, 1 | sbiev 2313 |
. . . . . . . . . . . . . 14
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜒) |
25 | | sbequ 2089 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
26 | 24, 25 | bitr3id 288 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → (𝜒 ↔ [𝑧 / 𝑥]𝜑)) |
27 | 26 | cbvralvw 3358 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝑥 𝜒 ↔ ∀𝑧 ∈ 𝑥 [𝑧 / 𝑥]𝜑) |
28 | | cbvralsvw 3377 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
suc 𝑦𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑) |
29 | 22, 27, 28 | 3bitr4g 317 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 ↔ ∀𝑥 ∈ suc 𝑦𝜑)) |
30 | 29 | imbi1d 345 |
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → ((∀𝑦 ∈ 𝑥 𝜒 → 𝜃) ↔ (∀𝑥 ∈ suc 𝑦𝜑 → 𝜃))) |
31 | 21, 30 | syl5ibrcom 250 |
. . . . . . . . 9
⊢ (𝑦 ∈ On → (𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜃))) |
32 | | tfinds.3 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) |
33 | 32 | biimprd 251 |
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑)) |
34 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ On → (𝑥 = suc 𝑦 → (𝜃 → 𝜑))) |
35 | 31, 34 | syldd 72 |
. . . . . . . 8
⊢ (𝑦 ∈ On → (𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))) |
36 | 15, 35 | rexlimi 3234 |
. . . . . . 7
⊢
(∃𝑦 ∈ On
𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)) |
37 | 12, 36 | jaoi 857 |
. . . . . 6
⊢ ((𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦) → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)) |
38 | 8, 37 | syl6 35 |
. . . . 5
⊢ (𝑥 ∈ On → ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))) |
39 | 5, 38 | syl5bir 246 |
. . . 4
⊢ (𝑥 ∈ On → (¬ (Ord
𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))) |
40 | 4, 39 | syl5bi 245 |
. . 3
⊢ (𝑥 ∈ On → (¬ Lim
𝑥 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))) |
41 | | tfinds.7 |
. . 3
⊢ (Lim
𝑥 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)) |
42 | 40, 41 | pm2.61d2 184 |
. 2
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)) |
43 | 1, 2, 42 | tfis3 7636 |
1
⊢ (𝐴 ∈ On → 𝜏) |