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 A \to Tr 𝒫 A$

Proof

Step	Hyp	Ref	Expression
1		dftr2	$⊢ Tr 𝒫 A \leftrightarrow \forall z \forall y ((z \in y \land y \in 𝒫 A) \to z \in 𝒫 A)$
2		idn1	$⊢ (Tr A \to Tr A)$
3		idn2	$⊢ (Tr A, (z \in y \land y \in 𝒫 A) \to (z \in y \land y \in 𝒫 A))$
4		simpr	$⊢ (z \in y \land y \in 𝒫 A) \to y \in 𝒫 A$
5	3 4	e2	$⊢ (Tr A, (z \in y \land y \in 𝒫 A) \to y \in 𝒫 A)$
6		elpwi	$⊢ y \in 𝒫 A \to y \subseteq A$
7	5 6	e2	$⊢ (Tr A, (z \in y \land y \in 𝒫 A) \to y \subseteq A)$
8		simpl	$⊢ (z \in y \land y \in 𝒫 A) \to z \in y$
9	3 8	e2	$⊢ (Tr A, (z \in y \land y \in 𝒫 A) \to z \in y)$
10		ssel	$⊢ y \subseteq A \to (z \in y \to z \in A)$
11	7 9 10	e22	$⊢ (Tr A, (z \in y \land y \in 𝒫 A) \to z \in A)$
12		trss	$⊢ Tr A \to (z \in A \to z \subseteq A)$
13	2 11 12	e12	$⊢ (Tr A, (z \in y \land y \in 𝒫 A) \to z \subseteq A)$
14		vex	$⊢ z \in V$
15	14	elpw	$⊢ z \in 𝒫 A \leftrightarrow z \subseteq A$
16	13 15	e2bir	$⊢ (Tr A, (z \in y \land y \in 𝒫 A) \to z \in 𝒫 A)$
17	16	in2	$⊢ (Tr A \to ((z \in y \land y \in 𝒫 A) \to z \in 𝒫 A))$
18	17	gen12	$⊢ (Tr A \to \forall z \forall y ((z \in y \land y \in 𝒫 A) \to z \in 𝒫 A))$
19		biimpr	$⊢ (Tr 𝒫 A \leftrightarrow \forall z \forall y ((z \in y \land y \in 𝒫 A) \to z \in 𝒫 A)) \to (\forall z \forall y ((z \in y \land y \in 𝒫 A) \to z \in 𝒫 A) \to Tr 𝒫 A)$
20	1 18 19	e01	$⊢ (Tr A \to Tr 𝒫 A)$
21	20	in1	$⊢ Tr A \to Tr 𝒫 A$

Metamath Proof Explorer

Theorem pwtrVD

Proof