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	⊢ 𝐴 ∈ V
Assertion	pwtrrVD	⊢ ( Tr 𝒫 𝐴 → Tr 𝐴 )

Proof

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