This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fpwwe2lem1

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 15-May-2015)

		Ref	Expression
	Hypothesis	fpwwe2.1	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y))\}$
	Assertion	fpwwe2lem1	$⊢ W \subseteq 𝒫 A \times 𝒫 (A \times A)$

Proof

Step	Hyp	Ref	Expression
1		fpwwe2.1	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y))\}$
2		simpll	$⊢ ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y)) \to x \subseteq A$
3		velpw	$⊢ x \in 𝒫 A \leftrightarrow x \subseteq A$
4	2 3	sylibr	$⊢ ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y)) \to x \in 𝒫 A$
5		simplr	$⊢ ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y)) \to r \subseteq x \times x$
6		xpss12	$⊢ (x \subseteq A \land x \subseteq A) \to x \times x \subseteq A \times A$
7	2 2 6	syl2anc	$⊢ ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y)) \to x \times x \subseteq A \times A$
8	5 7	sstrd	$⊢ ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y)) \to r \subseteq A \times A$
9		velpw	$⊢ r \in 𝒫 (A \times A) \leftrightarrow r \subseteq A \times A$
10	8 9	sylibr	$⊢ ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y)) \to r \in 𝒫 (A \times A)$
11	4 10	jca	$⊢ ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y)) \to (x \in 𝒫 A \land r \in 𝒫 (A \times A))$
12	11	ssopab2i	$⊢ \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y))\} \subseteq \{⟨x, r⟩ \| (x \in 𝒫 A \land r \in 𝒫 (A \times A))\}$
13		df-xp	$⊢ 𝒫 A \times 𝒫 (A \times A) = \{⟨x, r⟩ \| (x \in 𝒫 A \land r \in 𝒫 (A \times A))\}$
14	12 1 13	3sstr4i	$⊢ W \subseteq 𝒫 A \times 𝒫 (A \times A)$