fmucndlem

		Ref	Expression
	Assertion	fmucndlem	$⊢ (F Fn X \land A \subseteq X) \to (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) [A \times A] = F [A] \times F [A]$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$⊢ (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) [A \times A] = ran ({(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) ↾}_{(A \times A)})$
2		simpr	$⊢ (F Fn X \land A \subseteq X) \to A \subseteq X$
3		resmpo	$⊢ (A \subseteq X \land A \subseteq X) \to {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) ↾}_{(A \times A)} = (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩)$
4	2 3	sylancom	$⊢ (F Fn X \land A \subseteq X) \to {(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) ↾}_{(A \times A)} = (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩)$
5	4	rneqd	$⊢ (F Fn X \land A \subseteq X) \to ran ({(x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) ↾}_{(A \times A)}) = ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩)$
6	1 5	syl5eq	$⊢ (F Fn X \land A \subseteq X) \to (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) [A \times A] = ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩)$
7		vex	$⊢ x \in V$
8		vex	$⊢ y \in V$
9	7 8	op1std	$⊢ p = ⟨x, y⟩ \to 1^{st} (p) = x$
10	9	fveq2d	$⊢ p = ⟨x, y⟩ \to F (1^{st} (p)) = F (x)$
11	7 8	op2ndd	$⊢ p = ⟨x, y⟩ \to 2^{nd} (p) = y$
12	11	fveq2d	$⊢ p = ⟨x, y⟩ \to F (2^{nd} (p)) = F (y)$
13	10 12	opeq12d	$⊢ p = ⟨x, y⟩ \to ⟨F (1^{st} (p)), F (2^{nd} (p))⟩ = ⟨F (x), F (y)⟩$
14	13	mpompt	$⊢ (p \in (A \times A) ⟼ ⟨F (1^{st} (p)), F (2^{nd} (p))⟩) = (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩)$
15	14	eqcomi	$⊢ (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩) = (p \in (A \times A) ⟼ ⟨F (1^{st} (p)), F (2^{nd} (p))⟩)$
16	15	rneqi	$⊢ ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩) = ran (p \in (A \times A) ⟼ ⟨F (1^{st} (p)), F (2^{nd} (p))⟩)$
17		fvexd	$⊢ (⊤ \land p \in (A \times A)) \to F (1^{st} (p)) \in V$
18		fvexd	$⊢ (⊤ \land p \in (A \times A)) \to F (2^{nd} (p)) \in V$
19	16 17 18	fliftrel	$⊢ ⊤ \to ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩) \subseteq V \times V$
20	19	mptru	$⊢ ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩) \subseteq V \times V$
21	20	sseli	$⊢ p \in ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩) \to p \in (V \times V)$
22	21	adantl	$⊢ ((F Fn X \land A \subseteq X) \land p \in ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩)) \to p \in (V \times V)$
23		xpss	$⊢ F [A] \times F [A] \subseteq V \times V$
24	23	sseli	$⊢ p \in (F [A] \times F [A]) \to p \in (V \times V)$
25	24	adantl	$⊢ ((F Fn X \land A \subseteq X) \land p \in (F [A] \times F [A])) \to p \in (V \times V)$
26		fvelimab	$⊢ (F Fn X \land A \subseteq X) \to (1^{st} (p) \in F [A] \leftrightarrow \exists x \in A F (x) = 1^{st} (p))$
27		fvelimab	$⊢ (F Fn X \land A \subseteq X) \to (2^{nd} (p) \in F [A] \leftrightarrow \exists y \in A F (y) = 2^{nd} (p))$
28	26 27	anbi12d	$⊢ (F Fn X \land A \subseteq X) \to ((1^{st} (p) \in F [A] \land 2^{nd} (p) \in F [A]) \leftrightarrow (\exists x \in A F (x) = 1^{st} (p) \land \exists y \in A F (y) = 2^{nd} (p)))$
29		eqid	$⊢ (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩) = (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩)$
30		opex	$⊢ ⟨F (x), F (y)⟩ \in V$
31	29 30	elrnmpo	$⊢ ⟨1^{st} (p), 2^{nd} (p)⟩ \in ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩) \leftrightarrow \exists x \in A \exists y \in A ⟨1^{st} (p), 2^{nd} (p)⟩ = ⟨F (x), F (y)⟩$
32		eqcom	$⊢ ⟨1^{st} (p), 2^{nd} (p)⟩ = ⟨F (x), F (y)⟩ \leftrightarrow ⟨F (x), F (y)⟩ = ⟨1^{st} (p), 2^{nd} (p)⟩$
33		fvex	$⊢ 1^{st} (p) \in V$
34		fvex	$⊢ 2^{nd} (p) \in V$
35	33 34	opth2	$⊢ ⟨F (x), F (y)⟩ = ⟨1^{st} (p), 2^{nd} (p)⟩ \leftrightarrow (F (x) = 1^{st} (p) \land F (y) = 2^{nd} (p))$
36	32 35	bitri	$⊢ ⟨1^{st} (p), 2^{nd} (p)⟩ = ⟨F (x), F (y)⟩ \leftrightarrow (F (x) = 1^{st} (p) \land F (y) = 2^{nd} (p))$
37	36	2rexbii	$⊢ \exists x \in A \exists y \in A ⟨1^{st} (p), 2^{nd} (p)⟩ = ⟨F (x), F (y)⟩ \leftrightarrow \exists x \in A \exists y \in A (F (x) = 1^{st} (p) \land F (y) = 2^{nd} (p))$
38		reeanv	$⊢ \exists x \in A \exists y \in A (F (x) = 1^{st} (p) \land F (y) = 2^{nd} (p)) \leftrightarrow (\exists x \in A F (x) = 1^{st} (p) \land \exists y \in A F (y) = 2^{nd} (p))$
39	31 37 38	3bitri	$⊢ ⟨1^{st} (p), 2^{nd} (p)⟩ \in ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩) \leftrightarrow (\exists x \in A F (x) = 1^{st} (p) \land \exists y \in A F (y) = 2^{nd} (p))$
40	28 39	syl6rbbr	$⊢ (F Fn X \land A \subseteq X) \to (⟨1^{st} (p), 2^{nd} (p)⟩ \in ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩) \leftrightarrow (1^{st} (p) \in F [A] \land 2^{nd} (p) \in F [A]))$
41		opelxp	$⊢ ⟨1^{st} (p), 2^{nd} (p)⟩ \in (F [A] \times F [A]) \leftrightarrow (1^{st} (p) \in F [A] \land 2^{nd} (p) \in F [A])$
42	40 41	syl6bbr	$⊢ (F Fn X \land A \subseteq X) \to (⟨1^{st} (p), 2^{nd} (p)⟩ \in ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩) \leftrightarrow ⟨1^{st} (p), 2^{nd} (p)⟩ \in (F [A] \times F [A]))$
43	42	adantr	$⊢ ((F Fn X \land A \subseteq X) \land p \in (V \times V)) \to (⟨1^{st} (p), 2^{nd} (p)⟩ \in ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩) \leftrightarrow ⟨1^{st} (p), 2^{nd} (p)⟩ \in (F [A] \times F [A]))$
44		1st2nd2	$⊢ p \in (V \times V) \to p = ⟨1^{st} (p), 2^{nd} (p)⟩$
45	44	adantl	$⊢ ((F Fn X \land A \subseteq X) \land p \in (V \times V)) \to p = ⟨1^{st} (p), 2^{nd} (p)⟩$
46	45	eleq1d	$⊢ ((F Fn X \land A \subseteq X) \land p \in (V \times V)) \to (p \in ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩) \leftrightarrow ⟨1^{st} (p), 2^{nd} (p)⟩ \in ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩))$
47	45	eleq1d	$⊢ ((F Fn X \land A \subseteq X) \land p \in (V \times V)) \to (p \in (F [A] \times F [A]) \leftrightarrow ⟨1^{st} (p), 2^{nd} (p)⟩ \in (F [A] \times F [A]))$
48	43 46 47	3bitr4d	$⊢ ((F Fn X \land A \subseteq X) \land p \in (V \times V)) \to (p \in ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩) \leftrightarrow p \in (F [A] \times F [A]))$
49	22 25 48	eqrdav	$⊢ (F Fn X \land A \subseteq X) \to ran (x \in A, y \in A ⟼ ⟨F (x), F (y)⟩) = F [A] \times F [A]$
50	6 49	eqtrd	$⊢ (F Fn X \land A \subseteq X) \to (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩) [A \times A] = F [A] \times F [A]$

Metamath Proof Explorer

Theorem fmucndlem

Proof