| Step | Hyp | Ref
| Expression |
| 1 | | dftr2 5261 |
. . 3
⊢ (Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) |
| 2 | | idn1 44594 |
. . . . . . . 8
⊢ ( Tr 𝒫 𝐴 ▶ Tr
𝒫 𝐴 ) |
| 3 | | idn2 44633 |
. . . . . . . . 9
⊢ ( Tr 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ) |
| 4 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
| 5 | 3, 4 | e2 44651 |
. . . . . . . 8
⊢ ( Tr 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑦 ∈ 𝐴 ) |
| 6 | | pwtrrVD.1 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
| 7 | 6 | pwid 4622 |
. . . . . . . 8
⊢ 𝐴 ∈ 𝒫 𝐴 |
| 8 | | trel 5268 |
. . . . . . . . 9
⊢ (Tr
𝒫 𝐴 → ((𝑦 ∈ 𝐴 ∧ 𝐴 ∈ 𝒫 𝐴) → 𝑦 ∈ 𝒫 𝐴)) |
| 9 | 8 | expd 415 |
. . . . . . . 8
⊢ (Tr
𝒫 𝐴 → (𝑦 ∈ 𝐴 → (𝐴 ∈ 𝒫 𝐴 → 𝑦 ∈ 𝒫 𝐴))) |
| 10 | 2, 5, 7, 9 | e120 44683 |
. . . . . . 7
⊢ ( Tr 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑦 ∈ 𝒫 𝐴 ) |
| 11 | | elpwi 4607 |
. . . . . . 7
⊢ (𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴) |
| 12 | 10, 11 | e2 44651 |
. . . . . 6
⊢ ( Tr 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑦 ⊆ 𝐴 ) |
| 13 | | simpl 482 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝑦) |
| 14 | 3, 13 | e2 44651 |
. . . . . 6
⊢ ( Tr 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑧 ∈ 𝑦 ) |
| 15 | | ssel 3977 |
. . . . . 6
⊢ (𝑦 ⊆ 𝐴 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴)) |
| 16 | 12, 14, 15 | e22 44691 |
. . . . 5
⊢ ( Tr 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑧 ∈ 𝐴 ) |
| 17 | 16 | in2 44625 |
. . . 4
⊢ ( Tr 𝒫 𝐴 ▶ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) ) |
| 18 | 17 | gen12 44638 |
. . 3
⊢ ( Tr 𝒫 𝐴 ▶ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) ) |
| 19 | | biimpr 220 |
. . 3
⊢ ((Tr
𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) → (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) → Tr 𝐴)) |
| 20 | 1, 18, 19 | e01 44711 |
. 2
⊢ ( Tr 𝒫 𝐴 ▶ Tr 𝐴 ) |
| 21 | 20 | in1 44591 |
1
⊢ (Tr
𝒫 𝐴 → Tr 𝐴) |