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	bilani	$⊢ (F Fn A \land G Fn A) \to G = (x \in A ⟼ G (x))$
4		df-mpt	$⊢ (x \in A ⟼ G (x)) = \{⟨x, y⟩ \| (x \in A \land y = G (x))\}$
5	3 4	eqtrdi	$⊢ (F Fn A \land G Fn A) \to G = \{⟨x, y⟩ \| (x \in A \land y = G (x))\}$
6	1	marypha2lem2	$⊢ T = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$
7	6	a1i	$⊢ (F Fn A \land G Fn A) \to T = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$
8	5 7	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))\})$
9		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)))$
10	8 9	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))))$
11		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)))$
12		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)))$
13	12	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)))$
14		fvex	$⊢ G (x) \in V$
15		eleq1	$⊢ y = G (x) \to (y \in F (x) \leftrightarrow G (x) \in F (x))$
16	14 15	ceqsalv	$⊢ \forall y (y = G (x) \to y \in F (x)) \leftrightarrow G (x) \in F (x)$
17	16	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))$
18	11 13 17	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))$
19	18	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))$
20		df-ral	$⊢ \forall x \in A G (x) \in F (x) \leftrightarrow \forall x (x \in A \to G (x) \in F (x))$
21	19 20	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)$
22	10 21	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