Theorem sspwtrALT

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

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

Proof

Step	Hyp	Ref	Expression
1		dftr2	⊢ ( Tr 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
2		simpr	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
3		ssel	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝒫 𝐴 ) )
4		elpwi	⊢ ( 𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴 )
5	2 3 4	syl56	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ⊆ 𝐴 ) )
6		idd	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
7		simpl	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝑦 )
8	6 7	syl6	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝑦 ) )
9		ssel	⊢ ( 𝑦 ⊆ 𝐴 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴 ) )
10	5 8 9	syl6c	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
11	10	alrimivv	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
12		biimpr	⊢ ( ( Tr 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) → ( ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) → Tr 𝐴 ) )
13	1 11 12	mpsyl	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴 )
14	13	idiALT	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴 )