Step | Hyp | Ref
| Expression |
1 | | simpr 103 |
. . . . 5
⊢
((z ∈ y ∧ y ∈ suc A) →
y ∈ suc
A) |
2 | | vex 2554 |
. . . . . 6
⊢ y ∈
V |
3 | 2 | elsuc 4109 |
. . . . 5
⊢ (y ∈ suc A ↔ (y
∈ A ∨ y = A)) |
4 | 1, 3 | sylib 127 |
. . . 4
⊢
((z ∈ y ∧ y ∈ suc A) →
(y ∈
A ∨
y = A)) |
5 | | simpl 102 |
. . . . . . 7
⊢
((z ∈ y ∧ y ∈ suc A) →
z ∈
y) |
6 | | eleq2 2098 |
. . . . . . 7
⊢ (y = A →
(z ∈
y ↔ z ∈ A)) |
7 | 5, 6 | syl5ibcom 144 |
. . . . . 6
⊢
((z ∈ y ∧ y ∈ suc A) →
(y = A
→ z ∈ A)) |
8 | | elelsuc 4112 |
. . . . . 6
⊢ (z ∈ A → z ∈ suc A) |
9 | 7, 8 | syl6 29 |
. . . . 5
⊢
((z ∈ y ∧ y ∈ suc A) →
(y = A
→ z ∈ suc A)) |
10 | | trel 3852 |
. . . . . . . . 9
⊢ (Tr
A → ((z ∈ y ∧ y ∈ A) → z
∈ A)) |
11 | 10 | expd 245 |
. . . . . . . 8
⊢ (Tr
A → (z ∈ y → (y
∈ A
→ z ∈ A))) |
12 | 11 | adantrd 264 |
. . . . . . 7
⊢ (Tr
A → ((z ∈ y ∧ y ∈ suc A) → (y
∈ A
→ z ∈ A))) |
13 | 12, 8 | syl8 65 |
. . . . . 6
⊢ (Tr
A → ((z ∈ y ∧ y ∈ suc A) → (y
∈ A
→ z ∈ suc A))) |
14 | | jao 671 |
. . . . . 6
⊢
((y ∈ A →
z ∈ suc
A) → ((y = A →
z ∈ suc
A) → ((y ∈ A ∨ y = A) →
z ∈ suc
A))) |
15 | 13, 14 | syl6 29 |
. . . . 5
⊢ (Tr
A → ((z ∈ y ∧ y ∈ suc A) → ((y =
A → z ∈ suc A) → ((y
∈ A ∨ y = A) → z
∈ suc A)))) |
16 | 9, 15 | mpdi 38 |
. . . 4
⊢ (Tr
A → ((z ∈ y ∧ y ∈ suc A) → ((y
∈ A ∨ y = A) → z
∈ suc A))) |
17 | 4, 16 | mpdi 38 |
. . 3
⊢ (Tr
A → ((z ∈ y ∧ y ∈ suc A) → z
∈ suc A)) |
18 | 17 | alrimivv 1752 |
. 2
⊢ (Tr
A → ∀z∀y((z ∈ y ∧ y ∈ suc A) → z
∈ suc A)) |
19 | | dftr2 3847 |
. 2
⊢ (Tr suc
A ↔ ∀z∀y((z ∈ y ∧ y ∈ suc A) → z
∈ suc A)) |
20 | 18, 19 | sylibr 137 |
1
⊢ (Tr
A → Tr suc A) |