fparlem4

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

		Ref	Expression
	Assertion	fparlem4	$⊢ G Fn B \to {({2^{nd} ↾}_{(V \times V)})}^{-1} \circ (G \circ ({2^{nd} ↾}_{(V \times V)})) = ⋃_{y \in B} ((V \times \{y\}) \times (V \times \{G (y)\}))$

Proof

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

Metamath Proof Explorer

Theorem fparlem4

Proof