Step | Hyp | Ref
| Expression |
1 | | dftr2 5029 |
. . 3
⊢ (Tr suc
𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) |
2 | | sssucid 6104 |
. . . . . . . 8
⊢ 𝐴 ⊆ suc 𝐴 |
3 | | idn1 40361 |
. . . . . . . . 9
⊢ ( Tr 𝐴 ▶ Tr 𝐴 ) |
4 | | idn2 40400 |
. . . . . . . . . 10
⊢ ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ) |
5 | | simpl 475 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ 𝑦) |
6 | 4, 5 | e2 40418 |
. . . . . . . . 9
⊢ ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ 𝑧 ∈ 𝑦 ) |
7 | | idn3 40402 |
. . . . . . . . 9
⊢ ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 ∈ 𝐴 ▶ 𝑦 ∈ 𝐴 ) |
8 | | trel 5034 |
. . . . . . . . . 10
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) |
9 | 8 | expd 408 |
. . . . . . . . 9
⊢ (Tr 𝐴 → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))) |
10 | 3, 6, 7, 9 | e123 40549 |
. . . . . . . 8
⊢ ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 ∈ 𝐴 ▶ 𝑧 ∈ 𝐴 ) |
11 | | ssel 3847 |
. . . . . . . 8
⊢ (𝐴 ⊆ suc 𝐴 → (𝑧 ∈ 𝐴 → 𝑧 ∈ suc 𝐴)) |
12 | 2, 10, 11 | e03 40527 |
. . . . . . 7
⊢ ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 ∈ 𝐴 ▶ 𝑧 ∈ suc 𝐴 ) |
13 | 12 | in3 40396 |
. . . . . 6
⊢ ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) ) |
14 | | idn3 40402 |
. . . . . . . . 9
⊢ ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 = 𝐴 ▶ 𝑦 = 𝐴 ) |
15 | | eleq2 2849 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴)) |
16 | 15 | biimpcd 241 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑦 → (𝑦 = 𝐴 → 𝑧 ∈ 𝐴)) |
17 | 6, 14, 16 | e23 40542 |
. . . . . . . 8
⊢ ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 = 𝐴 ▶ 𝑧 ∈ 𝐴 ) |
18 | 2, 17, 11 | e03 40527 |
. . . . . . 7
⊢ ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 = 𝐴 ▶ 𝑧 ∈ suc 𝐴 ) |
19 | 18 | in3 40396 |
. . . . . 6
⊢ ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) ) |
20 | | simpr 477 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴) |
21 | 4, 20 | e2 40418 |
. . . . . . 7
⊢ ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ 𝑦 ∈ suc 𝐴 ) |
22 | | elsuci 6093 |
. . . . . . 7
⊢ (𝑦 ∈ suc 𝐴 → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) |
23 | 21, 22 | e2 40418 |
. . . . . 6
⊢ ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴) ) |
24 | | jao 944 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴))) |
25 | 13, 19, 23, 24 | e222 40423 |
. . . . 5
⊢ ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ 𝑧 ∈ suc 𝐴 ) |
26 | 25 | in2 40392 |
. . . 4
⊢ ( Tr 𝐴 ▶ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) ) |
27 | 26 | gen12 40405 |
. . 3
⊢ ( Tr 𝐴 ▶ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) ) |
28 | | biimpr 212 |
. . 3
⊢ ((Tr suc
𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) → (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) → Tr suc 𝐴)) |
29 | 1, 27, 28 | e01 40478 |
. 2
⊢ ( Tr 𝐴 ▶ Tr suc
𝐴 ) |
30 | 29 | in1 40358 |
1
⊢ (Tr 𝐴 → Tr suc 𝐴) |