Metamath Proof Explorer

Theorem pwtrrVD

Description: Virtual deduction proof of pwtr ; see pwtrVD for the converse. (Contributed by Alan Sare, 25-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis pwtrrVD.1 ⊢ A ∈ V
Assertion pwtrrVD ⊢ Tr ⁡ 𝒫 A → Tr ⁡ A

Proof

Step Hyp Ref Expression
1 pwtrrVD.1 ⊢ A ∈ V
2 dftr2 ⊢ Tr ⁡ A ↔ ∀ z ∀ y z ∈ y ∧ y ∈ A → z ∈ A
3 idn1 ⊢ Tr ⁡ 𝒫 A → Tr ⁡ 𝒫 A
4 idn2 ⊢ Tr ⁡ 𝒫 A , z ∈ y ∧ y ∈ A → z ∈ y ∧ y ∈ A
5 simpr ⊢ z ∈ y ∧ y ∈ A → y ∈ A
6 4 5 e2 ⊢ Tr ⁡ 𝒫 A , z ∈ y ∧ y ∈ A → y ∈ A
7 1 pwid ⊢ A ∈ 𝒫 A
8 trel ⊢ Tr ⁡ 𝒫 A → y ∈ A ∧ A ∈ 𝒫 A → y ∈ 𝒫 A
9 8 expd ⊢ Tr ⁡ 𝒫 A → y ∈ A → A ∈ 𝒫 A → y ∈ 𝒫 A
10 3 6 7 9 e120 ⊢ Tr ⁡ 𝒫 A , z ∈ y ∧ y ∈ A → y ∈ 𝒫 A
11 elpwi ⊢ y ∈ 𝒫 A → y ⊆ A
12 10 11 e2 ⊢ Tr ⁡ 𝒫 A , z ∈ y ∧ y ∈ A → y ⊆ A
13 simpl ⊢ z ∈ y ∧ y ∈ A → z ∈ y
14 4 13 e2 ⊢ Tr ⁡ 𝒫 A , z ∈ y ∧ y ∈ A → z ∈ y
15 ssel ⊢ y ⊆ A → z ∈ y → z ∈ A
16 12 14 15 e22 ⊢ Tr ⁡ 𝒫 A , z ∈ y ∧ y ∈ A → z ∈ A
17 16 in2 ⊢ Tr ⁡ 𝒫 A → z ∈ y ∧ y ∈ A → z ∈ A
18 17 gen12 ⊢ Tr ⁡ 𝒫 A → ∀ z ∀ y z ∈ y ∧ y ∈ A → z ∈ A
19 biimpr ⊢ Tr ⁡ A ↔ ∀ z ∀ y z ∈ y ∧ y ∈ A → z ∈ A → ∀ z ∀ y z ∈ y ∧ y ∈ A → z ∈ A → Tr ⁡ A
20 2 18 19 e01 ⊢ Tr ⁡ 𝒫 A → Tr ⁡ A
21 20 in1 ⊢ Tr ⁡ 𝒫 A → Tr ⁡ A