Theorem fparlem4 7167

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

Assertion

Ref	Expression
fparlem4	⊢ (𝐺 Fn 𝐵 → (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))) = ∪ 𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)})))

Distinct variable groups:   𝑦,𝐵   𝑦,𝐺

Proof of Theorem fparlem4

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		coiun 5562	. 2 ⊢ (◡(2nd ↾ (V × V)) ∘ ∪ 𝑦 ∈ 𝐵 ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦}))) = ∪ 𝑦 ∈ 𝐵 (◡(2nd ↾ (V × V)) ∘ ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦})))
2		inss1 3795	. . . . 5 ⊢ (dom 𝐺 ∩ ran (2nd ↾ (V × V))) ⊆ dom 𝐺
3		fndm 5904	. . . . 5 ⊢ (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵)
4	2, 3	syl5sseq 3616	. . . 4 ⊢ (𝐺 Fn 𝐵 → (dom 𝐺 ∩ ran (2nd ↾ (V × V))) ⊆ 𝐵)
5		dfco2a 5552	. . . 4 ⊢ ((dom 𝐺 ∩ ran (2nd ↾ (V × V))) ⊆ 𝐵 → (𝐺 ∘ (2nd ↾ (V × V))) = ∪ 𝑦 ∈ 𝐵 ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦})))
6	4, 5	syl 17	. . 3 ⊢ (𝐺 Fn 𝐵 → (𝐺 ∘ (2nd ↾ (V × V))) = ∪ 𝑦 ∈ 𝐵 ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦})))
7	6	coeq2d 5206	. 2 ⊢ (𝐺 Fn 𝐵 → (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))) = (◡(2nd ↾ (V × V)) ∘ ∪ 𝑦 ∈ 𝐵 ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦}))))
8		inss1 3795	. . . . . . . . 9 ⊢ (dom ({(𝐺‘𝑦)} × (V × {𝑦})) ∩ ran (2nd ↾ (V × V))) ⊆ dom ({(𝐺‘𝑦)} × (V × {𝑦}))
9		dmxpss 5484	. . . . . . . . 9 ⊢ dom ({(𝐺‘𝑦)} × (V × {𝑦})) ⊆ {(𝐺‘𝑦)}
10	8, 9	sstri 3577	. . . . . . . 8 ⊢ (dom ({(𝐺‘𝑦)} × (V × {𝑦})) ∩ ran (2nd ↾ (V × V))) ⊆ {(𝐺‘𝑦)}
11		dfco2a 5552	. . . . . . . 8 ⊢ ((dom ({(𝐺‘𝑦)} × (V × {𝑦})) ∩ ran (2nd ↾ (V × V))) ⊆ {(𝐺‘𝑦)} → (({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V × V))) = ∪ 𝑥 ∈ {(𝐺‘𝑦)} ((◡(2nd ↾ (V × V)) “ {𝑥}) × (({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥})))
12	10, 11	ax-mp 5	. . . . . . 7 ⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V × V))) = ∪ 𝑥 ∈ {(𝐺‘𝑦)} ((◡(2nd ↾ (V × V)) “ {𝑥}) × (({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥}))
13		fvex 6113	. . . . . . . 8 ⊢ (𝐺‘𝑦) ∈ V
14		fparlem2 7165	. . . . . . . . . 10 ⊢ (◡(2nd ↾ (V × V)) “ {𝑥}) = (V × {𝑥})
15		sneq 4135	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐺‘𝑦) → {𝑥} = {(𝐺‘𝑦)})
16	15	xpeq2d 5063	. . . . . . . . . 10 ⊢ (𝑥 = (𝐺‘𝑦) → (V × {𝑥}) = (V × {(𝐺‘𝑦)}))
17	14, 16	syl5eq 2656	. . . . . . . . 9 ⊢ (𝑥 = (𝐺‘𝑦) → (◡(2nd ↾ (V × V)) “ {𝑥}) = (V × {(𝐺‘𝑦)}))
18	15	imaeq2d 5385	. . . . . . . . . 10 ⊢ (𝑥 = (𝐺‘𝑦) → (({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥}) = (({(𝐺‘𝑦)} × (V × {𝑦})) “ {(𝐺‘𝑦)}))
19		df-ima 5051	. . . . . . . . . . 11 ⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) “ {(𝐺‘𝑦)}) = ran (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)})
20		ssid 3587	. . . . . . . . . . . . . 14 ⊢ {(𝐺‘𝑦)} ⊆ {(𝐺‘𝑦)}
21		xpssres 5354	. . . . . . . . . . . . . 14 ⊢ ({(𝐺‘𝑦)} ⊆ {(𝐺‘𝑦)} → (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = ({(𝐺‘𝑦)} × (V × {𝑦})))
22	20, 21	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = ({(𝐺‘𝑦)} × (V × {𝑦}))
23	22	rneqi 5273	. . . . . . . . . . . 12 ⊢ ran (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = ran ({(𝐺‘𝑦)} × (V × {𝑦}))
24	13	snnz 4252	. . . . . . . . . . . . 13 ⊢ {(𝐺‘𝑦)} ≠ ∅
25		rnxp 5483	. . . . . . . . . . . . 13 ⊢ ({(𝐺‘𝑦)} ≠ ∅ → ran ({(𝐺‘𝑦)} × (V × {𝑦})) = (V × {𝑦}))
26	24, 25	ax-mp 5	. . . . . . . . . . . 12 ⊢ ran ({(𝐺‘𝑦)} × (V × {𝑦})) = (V × {𝑦})
27	23, 26	eqtri 2632	. . . . . . . . . . 11 ⊢ ran (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = (V × {𝑦})
28	19, 27	eqtri 2632	. . . . . . . . . 10 ⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) “ {(𝐺‘𝑦)}) = (V × {𝑦})
29	18, 28	syl6eq 2660	. . . . . . . . 9 ⊢ (𝑥 = (𝐺‘𝑦) → (({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥}) = (V × {𝑦}))
30	17, 29	xpeq12d 5064	. . . . . . . 8 ⊢ (𝑥 = (𝐺‘𝑦) → ((◡(2nd ↾ (V × V)) “ {𝑥}) × (({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥})) = ((V × {(𝐺‘𝑦)}) × (V × {𝑦})))
31	13, 30	iunxsn 4539	. . . . . . 7 ⊢ ∪ 𝑥 ∈ {(𝐺‘𝑦)} ((◡(2nd ↾ (V × V)) “ {𝑥}) × (({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥})) = ((V × {(𝐺‘𝑦)}) × (V × {𝑦}))
32	12, 31	eqtri 2632	. . . . . 6 ⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V × V))) = ((V × {(𝐺‘𝑦)}) × (V × {𝑦}))
33	32	cnveqi 5219	. . . . 5 ⊢ ◡(({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V × V))) = ◡((V × {(𝐺‘𝑦)}) × (V × {𝑦}))
34		cnvco 5230	. . . . 5 ⊢ ◡(({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V × V))) = (◡(2nd ↾ (V × V)) ∘ ◡({(𝐺‘𝑦)} × (V × {𝑦})))
35		cnvxp 5470	. . . . 5 ⊢ ◡((V × {(𝐺‘𝑦)}) × (V × {𝑦})) = ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))
36	33, 34, 35	3eqtr3i 2640	. . . 4 ⊢ (◡(2nd ↾ (V × V)) ∘ ◡({(𝐺‘𝑦)} × (V × {𝑦}))) = ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))
37		fparlem2 7165	. . . . . . . . 9 ⊢ (◡(2nd ↾ (V × V)) “ {𝑦}) = (V × {𝑦})
38	37	xpeq2i 5060	. . . . . . . 8 ⊢ ({(𝐺‘𝑦)} × (◡(2nd ↾ (V × V)) “ {𝑦})) = ({(𝐺‘𝑦)} × (V × {𝑦}))
39		fnsnfv 6168	. . . . . . . . 9 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → {(𝐺‘𝑦)} = (𝐺 “ {𝑦}))
40	39	xpeq1d 5062	. . . . . . . 8 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ({(𝐺‘𝑦)} × (◡(2nd ↾ (V × V)) “ {𝑦})) = ((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V)) “ {𝑦})))
41	38, 40	syl5eqr 2658	. . . . . . 7 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ({(𝐺‘𝑦)} × (V × {𝑦})) = ((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V)) “ {𝑦})))
42	41	cnveqd 5220	. . . . . 6 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ◡({(𝐺‘𝑦)} × (V × {𝑦})) = ◡((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V)) “ {𝑦})))
43		cnvxp 5470	. . . . . 6 ⊢ ◡((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V)) “ {𝑦})) = ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦}))
44	42, 43	syl6eq 2660	. . . . 5 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ◡({(𝐺‘𝑦)} × (V × {𝑦})) = ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦})))
45	44	coeq2d 5206	. . . 4 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → (◡(2nd ↾ (V × V)) ∘ ◡({(𝐺‘𝑦)} × (V × {𝑦}))) = (◡(2nd ↾ (V × V)) ∘ ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦}))))
46	36, 45	syl5eqr 2658	. . 3 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ((V × {𝑦}) × (V × {(𝐺‘𝑦)})) = (◡(2nd ↾ (V × V)) ∘ ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦}))))
47	46	iuneq2dv 4478	. 2 ⊢ (𝐺 Fn 𝐵 → ∪ 𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)})) = ∪ 𝑦 ∈ 𝐵 (◡(2nd ↾ (V × V)) ∘ ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦}))))
48	1, 7, 47	3eqtr4a 2670	1 ⊢ (𝐺 Fn 𝐵 → (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))) = ∪ 𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)})))

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  {csn 4125  ∪ ciun 4455   × cxp 5036  ^◡ccnv 5037  dom cdm 5038  ran crn 5039   ↾ cres 5040   “ cima 5041   ∘ ccom 5042   Fn wfn 5799  ‘cfv 5804  2^nd c2nd 7058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-1st 7059  df-2nd 7060

This theorem is referenced by:  fpar  7168