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 𝐴 → Tr 𝒫 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dftr2	⊢ ( Tr 𝒫 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 ) → 𝑧 ∈ 𝒫 𝐴 ) )
2		idn1	⊢ (    Tr 𝐴    ▶    Tr 𝐴    )
3		idn2	⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 )    ▶    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 )    )
4		simpr	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 ) → 𝑦 ∈ 𝒫 𝐴 )
5	3 4	e2	⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 )    ▶    𝑦 ∈ 𝒫 𝐴    )
6		elpwi	⊢ ( 𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴 )
7	5 6	e2	⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 )    ▶    𝑦 ⊆ 𝐴    )
8		simpl	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 ) → 𝑧 ∈ 𝑦 )
9	3 8	e2	⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 )    ▶    𝑧 ∈ 𝑦    )
10		ssel	⊢ ( 𝑦 ⊆ 𝐴 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴 ) )
11	7 9 10	e22	⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 )    ▶    𝑧 ∈ 𝐴    )
12		trss	⊢ ( Tr 𝐴 → ( 𝑧 ∈ 𝐴 → 𝑧 ⊆ 𝐴 ) )
13	2 11 12	e12	⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 )    ▶    𝑧 ⊆ 𝐴    )
14		vex	⊢ 𝑧 ∈ V
15	14	elpw	⊢ ( 𝑧 ∈ 𝒫 𝐴 ↔ 𝑧 ⊆ 𝐴 )
16	13 15	e2bir	⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 )    ▶    𝑧 ∈ 𝒫 𝐴    )
17	16	in2	⊢ (    Tr 𝐴    ▶    ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 ) → 𝑧 ∈ 𝒫 𝐴 )    )
18	17	gen12	⊢ (    Tr 𝐴    ▶    ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 ) → 𝑧 ∈ 𝒫 𝐴 )    )
19		biimpr	⊢ ( ( Tr 𝒫 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 ) → 𝑧 ∈ 𝒫 𝐴 ) ) → ( ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 ) → 𝑧 ∈ 𝒫 𝐴 ) → Tr 𝒫 𝐴 ) )
20	1 18 19	e01	⊢ (    Tr 𝐴    ▶    Tr 𝒫 𝐴    )
21	20	in1	⊢ ( Tr 𝐴 → Tr 𝒫 𝐴 )