| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tfinds.2 | . 2
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) | 
| 2 |  | tfinds.4 | . 2
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) | 
| 3 |  | dflim3 7869 | . . . . 5
⊢ (Lim
𝑥 ↔ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦))) | 
| 4 | 3 | notbii 320 | . . . 4
⊢ (¬
Lim 𝑥 ↔ ¬ (Ord
𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦))) | 
| 5 |  | iman 401 | . . . . 5
⊢ ((Ord
𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) ↔ ¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦))) | 
| 6 |  | eloni 6393 | . . . . . . 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 258 | . . . . . . . 8
⊢ (𝑥 = ∅ → 𝜑) | 
| 12 | 11 | a1d 25 | . . . . . . 7
⊢ (𝑥 = ∅ → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)) | 
| 13 |  | nfra1 3283 | . . . . . . . . 9
⊢
Ⅎ𝑦∀𝑦 ∈ 𝑥 𝜒 | 
| 14 |  | nfv 1913 | . . . . . . . . 9
⊢
Ⅎ𝑦𝜑 | 
| 15 | 13, 14 | nfim 1895 | . . . . . . . 8
⊢
Ⅎ𝑦(∀𝑦 ∈ 𝑥 𝜒 → 𝜑) | 
| 16 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑦 ∈ V | 
| 17 | 16 | sucid 6465 | . . . . . . . . . . . 12
⊢ 𝑦 ∈ suc 𝑦 | 
| 18 | 1 | rspcv 3617 | . . . . . . . . . . . 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 3322 | . . . . . . . . . . . 12
⊢ (𝑥 = suc 𝑦 → (∀𝑧 ∈ 𝑥 [𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑)) | 
| 23 |  | nfv 1913 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥𝜒 | 
| 24 | 23, 1 | sbiev 2313 | . . . . . . . . . . . . . 14
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜒) | 
| 25 |  | sbequ 2082 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑)) | 
| 26 | 24, 25 | bitr3id 285 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → (𝜒 ↔ [𝑧 / 𝑥]𝜑)) | 
| 27 | 26 | cbvralvw 3236 | . . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝑥 𝜒 ↔ ∀𝑧 ∈ 𝑥 [𝑧 / 𝑥]𝜑) | 
| 28 |  | cbvralsvw 3316 | . . . . . . . . . . . 12
⊢
(∀𝑥 ∈
suc 𝑦𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑) | 
| 29 | 22, 27, 28 | 3bitr4g 314 | . . . . . . . . . . 11
⊢ (𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 ↔ ∀𝑥 ∈ suc 𝑦𝜑)) | 
| 30 | 29 | imbi1d 341 | . . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → ((∀𝑦 ∈ 𝑥 𝜒 → 𝜃) ↔ (∀𝑥 ∈ suc 𝑦𝜑 → 𝜃))) | 
| 31 | 21, 30 | syl5ibrcom 247 | . . . . . . . . 9
⊢ (𝑦 ∈ On → (𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜃))) | 
| 32 |  | tfinds.3 | . . . . . . . . . . 11
⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) | 
| 33 | 32 | biimprd 248 | . . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑)) | 
| 34 | 33 | a1i 11 | . . . . . . . . 9
⊢ (𝑦 ∈ On → (𝑥 = suc 𝑦 → (𝜃 → 𝜑))) | 
| 35 | 31, 34 | syldd 72 | . . . . . . . 8
⊢ (𝑦 ∈ On → (𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))) | 
| 36 | 15, 35 | rexlimi 3258 | . . . . . . 7
⊢
(∃𝑦 ∈ On
𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)) | 
| 37 | 12, 36 | jaoi 857 | . . . . . 6
⊢ ((𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦) → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)) | 
| 38 | 8, 37 | syl6 35 | . . . . 5
⊢ (𝑥 ∈ On → ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))) | 
| 39 | 5, 38 | biimtrrid 243 | . . . 4
⊢ (𝑥 ∈ On → (¬ (Ord
𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))) | 
| 40 | 4, 39 | biimtrid 242 | . . 3
⊢ (𝑥 ∈ On → (¬ Lim
𝑥 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))) | 
| 41 |  | tfinds.7 | . . 3
⊢ (Lim
𝑥 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)) | 
| 42 | 40, 41 | pm2.61d2 181 | . 2
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)) | 
| 43 | 1, 2, 42 | tfis3 7880 | 1
⊢ (𝐴 ∈ On → 𝜏) |