Metamath Proof Explorer

Theorem pwtrVD

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

Ref Expression
Assertion pwtrVD ⊢ Tr ⁡ A → Tr ⁡ 𝒫 A

Proof

Step Hyp Ref Expression
1 dftr2 ⊢ Tr ⁡ 𝒫 A ↔ ∀ z ∀ y z ∈ y ∧ y ∈ 𝒫 A → z ∈ 𝒫 A
2 idn1 ⊢ Tr ⁡ A → Tr ⁡ A
3 idn2 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ 𝒫 A → z ∈ y ∧ y ∈ 𝒫 A
4 simpr ⊢ z ∈ y ∧ y ∈ 𝒫 A → y ∈ 𝒫 A
5 3 4 e2 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ 𝒫 A → y ∈ 𝒫 A
6 elpwi ⊢ y ∈ 𝒫 A → y ⊆ A
7 5 6 e2 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ 𝒫 A → y ⊆ A
8 simpl ⊢ z ∈ y ∧ y ∈ 𝒫 A → z ∈ y
9 3 8 e2 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ 𝒫 A → z ∈ y
10 ssel ⊢ y ⊆ A → z ∈ y → z ∈ A
11 7 9 10 e22 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ 𝒫 A → z ∈ A
12 trss ⊢ Tr ⁡ A → z ∈ A → z ⊆ A
13 2 11 12 e12 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ 𝒫 A → z ⊆ A
14 vex ⊢ z ∈ V
15 14 elpw ⊢ z ∈ 𝒫 A ↔ z ⊆ A
16 13 15 e2bir ⊢ 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 1 18 19 e01 ⊢ Tr ⁡ A → Tr ⁡ 𝒫 A
21 20 in1 ⊢ Tr ⁡ A → Tr ⁡ 𝒫 A