Theorem trsspwALT

Description: Virtual deduction proof of the left-to-right implication of dftr4 . A transitive class is a subset of its power class. This proof corresponds to the virtual deduction proof of dftr4 without accumulating results. (Contributed by Alan Sare, 29-Apr-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	trsspwALT	⊢ ( Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dfss2	⊢ ( 𝐴 ⊆ 𝒫 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴 ) )
2		idn1	⊢ (    Tr 𝐴    ▶    Tr 𝐴    )
3		idn2	⊢ (    Tr 𝐴    ,    𝑥 ∈ 𝐴    ▶    𝑥 ∈ 𝐴    )
4		trss	⊢ ( Tr 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴 ) )
5	2 3 4	e12	⊢ (    Tr 𝐴    ,    𝑥 ∈ 𝐴    ▶    𝑥 ⊆ 𝐴    )
6		vex	⊢ 𝑥 ∈ V
7	6	elpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
8	5 7	e2bir	⊢ (    Tr 𝐴    ,    𝑥 ∈ 𝐴    ▶    𝑥 ∈ 𝒫 𝐴    )
9	8	in2	⊢ (    Tr 𝐴    ▶    ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴 )    )
10	9	gen11	⊢ (    Tr 𝐴    ▶    ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴 )    )
11		biimpr	⊢ ( ( 𝐴 ⊆ 𝒫 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴 ) ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴 ) → 𝐴 ⊆ 𝒫 𝐴 ) )
12	1 10 11	e01	⊢ (    Tr 𝐴    ▶    𝐴 ⊆ 𝒫 𝐴    )
13	12	in1	⊢ ( Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴 )