fparlem3

Description: Lemma for fpar . (Contributed by NM, 22-Dec-2008) (Revised by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	fparlem3	$⊢ F Fn A \to {({1^{st} ↾}_{(V \times V)})}^{-1} \circ (F \circ ({1^{st} ↾}_{(V \times V)})) = ⋃_{x \in A} ((\{x\} \times V) \times (\{F (x)\} \times V))$

Proof

Step	Hyp	Ref	Expression
1		coiun	$⊢ {({1^{st} ↾}_{(V \times V)})}^{-1} \circ ⋃_{x \in A} ({({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] \times F [\{x\}]) = ⋃_{x \in A} ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ ({({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] \times F [\{x\}]))$
2		inss1	$⊢ dom F \cap ran ({1^{st} ↾}_{(V \times V)}) \subseteq dom F$
3		fndm	$⊢ F Fn A \to dom F = A$
4	2 3	sseqtrid	$⊢ F Fn A \to dom F \cap ran ({1^{st} ↾}_{(V \times V)}) \subseteq A$
5		dfco2a	$⊢ dom F \cap ran ({1^{st} ↾}_{(V \times V)}) \subseteq A \to F \circ ({1^{st} ↾}_{(V \times V)}) = ⋃_{x \in A} ({({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] \times F [\{x\}])$
6	4 5	syl	$⊢ F Fn A \to F \circ ({1^{st} ↾}_{(V \times V)}) = ⋃_{x \in A} ({({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] \times F [\{x\}])$
7	6	coeq2d	$⊢ F Fn A \to {({1^{st} ↾}_{(V \times V)})}^{-1} \circ (F \circ ({1^{st} ↾}_{(V \times V)})) = {({1^{st} ↾}_{(V \times V)})}^{-1} \circ ⋃_{x \in A} ({({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] \times F [\{x\}])$
8		inss1	$⊢ dom (\{F (x)\} \times (\{x\} \times V)) \cap ran ({1^{st} ↾}_{(V \times V)}) \subseteq dom (\{F (x)\} \times (\{x\} \times V))$
9		dmxpss	$⊢ dom (\{F (x)\} \times (\{x\} \times V)) \subseteq \{F (x)\}$
10	8 9	sstri	$⊢ dom (\{F (x)\} \times (\{x\} \times V)) \cap ran ({1^{st} ↾}_{(V \times V)}) \subseteq \{F (x)\}$
11		dfco2a	$⊢ dom (\{F (x)\} \times (\{x\} \times V)) \cap ran ({1^{st} ↾}_{(V \times V)}) \subseteq \{F (x)\} \to (\{F (x)\} \times (\{x\} \times V)) \circ ({1^{st} ↾}_{(V \times V)}) = ⋃_{y \in \{F (x)\}} ({({1^{st} ↾}_{(V \times V)})}^{-1} [\{y\}] \times (\{F (x)\} \times (\{x\} \times V)) [\{y\}])$
12	10 11	ax-mp	$⊢ (\{F (x)\} \times (\{x\} \times V)) \circ ({1^{st} ↾}_{(V \times V)}) = ⋃_{y \in \{F (x)\}} ({({1^{st} ↾}_{(V \times V)})}^{-1} [\{y\}] \times (\{F (x)\} \times (\{x\} \times V)) [\{y\}])$
13		fvex	$⊢ F (x) \in V$
14		fparlem1	$⊢ {({1^{st} ↾}_{(V \times V)})}^{-1} [\{y\}] = \{y\} \times V$
15		sneq	$⊢ y = F (x) \to \{y\} = \{F (x)\}$
16	15	xpeq1d	$⊢ y = F (x) \to \{y\} \times V = \{F (x)\} \times V$
17	14 16	eqtrid	$⊢ y = F (x) \to {({1^{st} ↾}_{(V \times V)})}^{-1} [\{y\}] = \{F (x)\} \times V$
18	15	imaeq2d	$⊢ y = F (x) \to (\{F (x)\} \times (\{x\} \times V)) [\{y\}] = (\{F (x)\} \times (\{x\} \times V)) [\{F (x)\}]$
19		df-ima	$⊢ (\{F (x)\} \times (\{x\} \times V)) [\{F (x)\}] = ran ({(\{F (x)\} \times (\{x\} \times V)) ↾}_{\{F (x)\}})$
20		ssid	$⊢ \{F (x)\} \subseteq \{F (x)\}$
21		xpssres	$⊢ \{F (x)\} \subseteq \{F (x)\} \to {(\{F (x)\} \times (\{x\} \times V)) ↾}_{\{F (x)\}} = \{F (x)\} \times (\{x\} \times V)$
22	20 21	ax-mp	$⊢ {(\{F (x)\} \times (\{x\} \times V)) ↾}_{\{F (x)\}} = \{F (x)\} \times (\{x\} \times V)$
23	22	rneqi	$⊢ ran ({(\{F (x)\} \times (\{x\} \times V)) ↾}_{\{F (x)\}}) = ran (\{F (x)\} \times (\{x\} \times V))$
24	13	snnz	$⊢ \{F (x)\} \neq \emptyset$
25		rnxp	$⊢ \{F (x)\} \neq \emptyset \to ran (\{F (x)\} \times (\{x\} \times V)) = \{x\} \times V$
26	24 25	ax-mp	$⊢ ran (\{F (x)\} \times (\{x\} \times V)) = \{x\} \times V$
27	23 26	eqtri	$⊢ ran ({(\{F (x)\} \times (\{x\} \times V)) ↾}_{\{F (x)\}}) = \{x\} \times V$
28	19 27	eqtri	$⊢ (\{F (x)\} \times (\{x\} \times V)) [\{F (x)\}] = \{x\} \times V$
29	18 28	eqtrdi	$⊢ y = F (x) \to (\{F (x)\} \times (\{x\} \times V)) [\{y\}] = \{x\} \times V$
30	17 29	xpeq12d	$⊢ y = F (x) \to {({1^{st} ↾}_{(V \times V)})}^{-1} [\{y\}] \times (\{F (x)\} \times (\{x\} \times V)) [\{y\}] = (\{F (x)\} \times V) \times (\{x\} \times V)$
31	13 30	iunxsn	$⊢ ⋃_{y \in \{F (x)\}} ({({1^{st} ↾}_{(V \times V)})}^{-1} [\{y\}] \times (\{F (x)\} \times (\{x\} \times V)) [\{y\}]) = (\{F (x)\} \times V) \times (\{x\} \times V)$
32	12 31	eqtri	$⊢ (\{F (x)\} \times (\{x\} \times V)) \circ ({1^{st} ↾}_{(V \times V)}) = (\{F (x)\} \times V) \times (\{x\} \times V)$
33	32	cnveqi	$⊢ {((\{F (x)\} \times (\{x\} \times V)) \circ ({1^{st} ↾}_{(V \times V)}))}^{-1} = {((\{F (x)\} \times V) \times (\{x\} \times V))}^{-1}$
34		cnvco	$⊢ {((\{F (x)\} \times (\{x\} \times V)) \circ ({1^{st} ↾}_{(V \times V)}))}^{-1} = {({1^{st} ↾}_{(V \times V)})}^{-1} \circ {(\{F (x)\} \times (\{x\} \times V))}^{-1}$
35		cnvxp	$⊢ {((\{F (x)\} \times V) \times (\{x\} \times V))}^{-1} = (\{x\} \times V) \times (\{F (x)\} \times V)$
36	33 34 35	3eqtr3i	$⊢ {({1^{st} ↾}_{(V \times V)})}^{-1} \circ {(\{F (x)\} \times (\{x\} \times V))}^{-1} = (\{x\} \times V) \times (\{F (x)\} \times V)$
37		fparlem1	$⊢ {({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] = \{x\} \times V$
38	37	xpeq2i	$⊢ \{F (x)\} \times {({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] = \{F (x)\} \times (\{x\} \times V)$
39		fnsnfv	$⊢ (F Fn A \land x \in A) \to \{F (x)\} = F [\{x\}]$
40	39	xpeq1d	$⊢ (F Fn A \land x \in A) \to \{F (x)\} \times {({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] = F [\{x\}] \times {({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}]$
41	38 40	eqtr3id	$⊢ (F Fn A \land x \in A) \to \{F (x)\} \times (\{x\} \times V) = F [\{x\}] \times {({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}]$
42	41	cnveqd	$⊢ (F Fn A \land x \in A) \to {(\{F (x)\} \times (\{x\} \times V))}^{-1} = {(F [\{x\}] \times {({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}])}^{-1}$
43		cnvxp	$⊢ {(F [\{x\}] \times {({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}])}^{-1} = {({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] \times F [\{x\}]$
44	42 43	eqtrdi	$⊢ (F Fn A \land x \in A) \to {(\{F (x)\} \times (\{x\} \times V))}^{-1} = {({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] \times F [\{x\}]$
45	44	coeq2d	$⊢ (F Fn A \land x \in A) \to {({1^{st} ↾}_{(V \times V)})}^{-1} \circ {(\{F (x)\} \times (\{x\} \times V))}^{-1} = {({1^{st} ↾}_{(V \times V)})}^{-1} \circ ({({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] \times F [\{x\}])$
46	36 45	eqtr3id	$⊢ (F Fn A \land x \in A) \to (\{x\} \times V) \times (\{F (x)\} \times V) = {({1^{st} ↾}_{(V \times V)})}^{-1} \circ ({({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] \times F [\{x\}])$
47	46	iuneq2dv	$⊢ F Fn A \to ⋃_{x \in A} ((\{x\} \times V) \times (\{F (x)\} \times V)) = ⋃_{x \in A} ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ ({({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] \times F [\{x\}]))$
48	1 7 47	3eqtr4a	$⊢ F Fn A \to {({1^{st} ↾}_{(V \times V)})}^{-1} \circ (F \circ ({1^{st} ↾}_{(V \times V)})) = ⋃_{x \in A} ((\{x\} \times V) \times (\{F (x)\} \times V))$

Metamath Proof Explorer

Theorem fparlem3

Proof