marypha2lem3

Description: Lemma for marypha2 . Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015)

		Ref	Expression
	Hypothesis	marypha2lem.t	$⊢ T = ⋃_{x \in A} (\{x\} \times F (x))$
	Assertion	marypha2lem3	$⊢ (F Fn A \land G Fn A) \to (G \subseteq T \leftrightarrow \forall x \in A G (x) \in F (x))$

Proof

Step	Hyp	Ref	Expression
1		marypha2lem.t	$⊢ T = ⋃_{x \in A} (\{x\} \times F (x))$
2		dffn5	$⊢ G Fn A \leftrightarrow G = (x \in A ⟼ G (x))$
3	2	biimpi	$⊢ G Fn A \to G = (x \in A ⟼ G (x))$
4	3	adantl	$⊢ (F Fn A \land G Fn A) \to G = (x \in A ⟼ G (x))$
5		df-mpt	$⊢ (x \in A ⟼ G (x)) = \{⟨x, y⟩ \| (x \in A \land y = G (x))\}$
6	4 5	eqtrdi	$⊢ (F Fn A \land G Fn A) \to G = \{⟨x, y⟩ \| (x \in A \land y = G (x))\}$
7	1	marypha2lem2	$⊢ T = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$
8	7	a1i	$⊢ (F Fn A \land G Fn A) \to T = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$
9	6 8	sseq12d	$⊢ (F Fn A \land G Fn A) \to (G \subseteq T \leftrightarrow \{⟨x, y⟩ \| (x \in A \land y = G (x))\} \subseteq \{⟨x, y⟩ \| (x \in A \land y \in F (x))\})$
10		ssopab2bw	$⊢ \{⟨x, y⟩ \| (x \in A \land y = G (x))\} \subseteq \{⟨x, y⟩ \| (x \in A \land y \in F (x))\} \leftrightarrow \forall x \forall y ((x \in A \land y = G (x)) \to (x \in A \land y \in F (x)))$
11	9 10	bitrdi	$⊢ (F Fn A \land G Fn A) \to (G \subseteq T \leftrightarrow \forall x \forall y ((x \in A \land y = G (x)) \to (x \in A \land y \in F (x))))$
12		19.21v	$⊢ \forall y (x \in A \to (y = G (x) \to y \in F (x))) \leftrightarrow (x \in A \to \forall y (y = G (x) \to y \in F (x)))$
13		imdistan	$⊢ (x \in A \to (y = G (x) \to y \in F (x))) \leftrightarrow ((x \in A \land y = G (x)) \to (x \in A \land y \in F (x)))$
14	13	albii	$⊢ \forall y (x \in A \to (y = G (x) \to y \in F (x))) \leftrightarrow \forall y ((x \in A \land y = G (x)) \to (x \in A \land y \in F (x)))$
15		fvex	$⊢ G (x) \in V$
16		eleq1	$⊢ y = G (x) \to (y \in F (x) \leftrightarrow G (x) \in F (x))$
17	15 16	ceqsalv	$⊢ \forall y (y = G (x) \to y \in F (x)) \leftrightarrow G (x) \in F (x)$
18	17	imbi2i	$⊢ (x \in A \to \forall y (y = G (x) \to y \in F (x))) \leftrightarrow (x \in A \to G (x) \in F (x))$
19	12 14 18	3bitr3i	$⊢ \forall y ((x \in A \land y = G (x)) \to (x \in A \land y \in F (x))) \leftrightarrow (x \in A \to G (x) \in F (x))$
20	19	albii	$⊢ \forall x \forall y ((x \in A \land y = G (x)) \to (x \in A \land y \in F (x))) \leftrightarrow \forall x (x \in A \to G (x) \in F (x))$
21		df-ral	$⊢ \forall x \in A G (x) \in F (x) \leftrightarrow \forall x (x \in A \to G (x) \in F (x))$
22	20 21	bitr4i	$⊢ \forall x \forall y ((x \in A \land y = G (x)) \to (x \in A \land y \in F (x))) \leftrightarrow \forall x \in A G (x) \in F (x)$
23	11 22	bitrdi	$⊢ (F Fn A \land G Fn A) \to (G \subseteq T \leftrightarrow \forall x \in A G (x) \in F (x))$

Metamath Proof Explorer

Theorem marypha2lem3

Proof