Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . . 5
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴) |
2 | | vex 3203 |
. . . . . 6
⊢ 𝑦 ∈ V |
3 | 2 | elsuc 5794 |
. . . . 5
⊢ (𝑦 ∈ suc 𝐴 ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) |
4 | 1, 3 | sylib 208 |
. . . 4
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) |
5 | | simpl 473 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ 𝑦) |
6 | | eleq2 2690 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴)) |
7 | 5, 6 | syl5ibcom 235 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 = 𝐴 → 𝑧 ∈ 𝐴)) |
8 | | elelsuc 5797 |
. . . . . 6
⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) |
9 | 7, 8 | syl6 35 |
. . . . 5
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴)) |
10 | | trel 4759 |
. . . . . . . . 9
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) |
11 | 10 | expd 452 |
. . . . . . . 8
⊢ (Tr 𝐴 → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))) |
12 | 11 | adantrd 484 |
. . . . . . 7
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))) |
13 | 12, 8 | syl8 76 |
. . . . . 6
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴))) |
14 | | jao 534 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴))) |
15 | 13, 14 | syl6 35 |
. . . . 5
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → ((𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴)))) |
16 | 9, 15 | mpdi 45 |
. . . 4
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → ((𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴))) |
17 | 4, 16 | mpdi 45 |
. . 3
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) |
18 | 17 | alrimivv 1856 |
. 2
⊢ (Tr 𝐴 → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) |
19 | | dftr2 4754 |
. 2
⊢ (Tr suc
𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) |
20 | 18, 19 | sylibr 224 |
1
⊢ (Tr 𝐴 → Tr suc 𝐴) |