Theorem trsspwALT2

Description: Virtual deduction proof of trsspwALT . This proof is the same as the proof of trsspwALT except each virtual deduction symbol is replaced by its non-virtual deduction symbol equivalent. A transitive class is a subset of its power class. (Contributed by Alan Sare, 23-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dfss2	⊢ ( 𝐴 ⊆ 𝒫 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴 ) )
2		id	⊢ ( Tr 𝐴 → Tr 𝐴 )
3		idd	⊢ ( Tr 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴 ) )
4		trss	⊢ ( Tr 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴 ) )
5	2 3 4	sylsyld	⊢ ( Tr 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴 ) )
6		vex	⊢ 𝑥 ∈ V
7	6	elpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
8	5 7	syl6ibr	⊢ ( Tr 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴 ) )
9	8	idiALT	⊢ ( Tr 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴 ) )
10	9	alrimiv	⊢ ( Tr 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴 ) )
11		biimpr	⊢ ( ( 𝐴 ⊆ 𝒫 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴 ) ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴 ) → 𝐴 ⊆ 𝒫 𝐴 ) )
12	1 10 11	mpsyl	⊢ ( Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴 )
13	12	idiALT	⊢ ( Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴 )