Theorem fparlem4 8095

Description: Lemma for fpar 8096. (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 6245	. 2 ⊢ (◡(2nd ↾ (V × V)) ∘ ∪ 𝑦 ∈ 𝐵 ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦}))) = ∪ 𝑦 ∈ 𝐵 (◡(2nd ↾ (V × V)) ∘ ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦})))
2		inss1 4220	. . . . 5 ⊢ (dom 𝐺 ∩ ran (2nd ↾ (V × V))) ⊆ dom 𝐺
3		fndm 6642	. . . . 5 ⊢ (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵)
4	2, 3	sseqtrid 4026	. . . 4 ⊢ (𝐺 Fn 𝐵 → (dom 𝐺 ∩ ran (2nd ↾ (V × V))) ⊆ 𝐵)
5		dfco2a 6235	. . . 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 5852	. 2 ⊢ (𝐺 Fn 𝐵 → (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))) = (◡(2nd ↾ (V × V)) ∘ ∪ 𝑦 ∈ 𝐵 ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦}))))
8		inss1 4220	. . . . . . . . 9 ⊢ (dom ({(𝐺‘𝑦)} × (V × {𝑦})) ∩ ran (2nd ↾ (V × V))) ⊆ dom ({(𝐺‘𝑦)} × (V × {𝑦}))
9		dmxpss 6160	. . . . . . . . 9 ⊢ dom ({(𝐺‘𝑦)} × (V × {𝑦})) ⊆ {(𝐺‘𝑦)}
10	8, 9	sstri 3983	. . . . . . . 8 ⊢ (dom ({(𝐺‘𝑦)} × (V × {𝑦})) ∩ ran (2nd ↾ (V × V))) ⊆ {(𝐺‘𝑦)}
11		dfco2a 6235	. . . . . . . 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 6894	. . . . . . . 8 ⊢ (𝐺‘𝑦) ∈ V
14		fparlem2 8093	. . . . . . . . . 10 ⊢ (◡(2nd ↾ (V × V)) “ {𝑥}) = (V × {𝑥})
15		sneq 4630	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐺‘𝑦) → {𝑥} = {(𝐺‘𝑦)})
16	15	xpeq2d 5696	. . . . . . . . . 10 ⊢ (𝑥 = (𝐺‘𝑦) → (V × {𝑥}) = (V × {(𝐺‘𝑦)}))
17	14, 16	eqtrid 2776	. . . . . . . . 9 ⊢ (𝑥 = (𝐺‘𝑦) → (◡(2nd ↾ (V × V)) “ {𝑥}) = (V × {(𝐺‘𝑦)}))
18	15	imaeq2d 6049	. . . . . . . . . 10 ⊢ (𝑥 = (𝐺‘𝑦) → (({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥}) = (({(𝐺‘𝑦)} × (V × {𝑦})) “ {(𝐺‘𝑦)}))
19		df-ima 5679	. . . . . . . . . . 11 ⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) “ {(𝐺‘𝑦)}) = ran (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)})
20		ssid 3996	. . . . . . . . . . . . . 14 ⊢ {(𝐺‘𝑦)} ⊆ {(𝐺‘𝑦)}
21		xpssres 6008	. . . . . . . . . . . . . 14 ⊢ ({(𝐺‘𝑦)} ⊆ {(𝐺‘𝑦)} → (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = ({(𝐺‘𝑦)} × (V × {𝑦})))
22	20, 21	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = ({(𝐺‘𝑦)} × (V × {𝑦}))
23	22	rneqi 5926	. . . . . . . . . . . 12 ⊢ ran (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = ran ({(𝐺‘𝑦)} × (V × {𝑦}))
24	13	snnz 4772	. . . . . . . . . . . . 13 ⊢ {(𝐺‘𝑦)} ≠ ∅
25		rnxp 6159	. . . . . . . . . . . . 13 ⊢ ({(𝐺‘𝑦)} ≠ ∅ → ran ({(𝐺‘𝑦)} × (V × {𝑦})) = (V × {𝑦}))
26	24, 25	ax-mp 5	. . . . . . . . . . . 12 ⊢ ran ({(𝐺‘𝑦)} × (V × {𝑦})) = (V × {𝑦})
27	23, 26	eqtri 2752	. . . . . . . . . . 11 ⊢ ran (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = (V × {𝑦})
28	19, 27	eqtri 2752	. . . . . . . . . 10 ⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) “ {(𝐺‘𝑦)}) = (V × {𝑦})
29	18, 28	eqtrdi 2780	. . . . . . . . 9 ⊢ (𝑥 = (𝐺‘𝑦) → (({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥}) = (V × {𝑦}))
30	17, 29	xpeq12d 5697	. . . . . . . 8 ⊢ (𝑥 = (𝐺‘𝑦) → ((◡(2nd ↾ (V × V)) “ {𝑥}) × (({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥})) = ((V × {(𝐺‘𝑦)}) × (V × {𝑦})))
31	13, 30	iunxsn 5084	. . . . . . 7 ⊢ ∪ 𝑥 ∈ {(𝐺‘𝑦)} ((◡(2nd ↾ (V × V)) “ {𝑥}) × (({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥})) = ((V × {(𝐺‘𝑦)}) × (V × {𝑦}))
32	12, 31	eqtri 2752	. . . . . 6 ⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V × V))) = ((V × {(𝐺‘𝑦)}) × (V × {𝑦}))
33	32	cnveqi 5864	. . . . 5 ⊢ ◡(({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V × V))) = ◡((V × {(𝐺‘𝑦)}) × (V × {𝑦}))
34		cnvco 5875	. . . . 5 ⊢ ◡(({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V × V))) = (◡(2nd ↾ (V × V)) ∘ ◡({(𝐺‘𝑦)} × (V × {𝑦})))
35		cnvxp 6146	. . . . 5 ⊢ ◡((V × {(𝐺‘𝑦)}) × (V × {𝑦})) = ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))
36	33, 34, 35	3eqtr3i 2760	. . . 4 ⊢ (◡(2nd ↾ (V × V)) ∘ ◡({(𝐺‘𝑦)} × (V × {𝑦}))) = ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))
37		fparlem2 8093	. . . . . . . . 9 ⊢ (◡(2nd ↾ (V × V)) “ {𝑦}) = (V × {𝑦})
38	37	xpeq2i 5693	. . . . . . . 8 ⊢ ({(𝐺‘𝑦)} × (◡(2nd ↾ (V × V)) “ {𝑦})) = ({(𝐺‘𝑦)} × (V × {𝑦}))
39		fnsnfv 6960	. . . . . . . . 9 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → {(𝐺‘𝑦)} = (𝐺 “ {𝑦}))
40	39	xpeq1d 5695	. . . . . . . 8 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ({(𝐺‘𝑦)} × (◡(2nd ↾ (V × V)) “ {𝑦})) = ((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V)) “ {𝑦})))
41	38, 40	eqtr3id 2778	. . . . . . 7 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ({(𝐺‘𝑦)} × (V × {𝑦})) = ((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V)) “ {𝑦})))
42	41	cnveqd 5865	. . . . . 6 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ◡({(𝐺‘𝑦)} × (V × {𝑦})) = ◡((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V)) “ {𝑦})))
43		cnvxp 6146	. . . . . 6 ⊢ ◡((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V)) “ {𝑦})) = ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦}))
44	42, 43	eqtrdi 2780	. . . . 5 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ◡({(𝐺‘𝑦)} × (V × {𝑦})) = ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦})))
45	44	coeq2d 5852	. . . 4 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → (◡(2nd ↾ (V × V)) ∘ ◡({(𝐺‘𝑦)} × (V × {𝑦}))) = (◡(2nd ↾ (V × V)) ∘ ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦}))))
46	36, 45	eqtr3id 2778	. . 3 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ((V × {𝑦}) × (V × {(𝐺‘𝑦)})) = (◡(2nd ↾ (V × V)) ∘ ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦}))))
47	46	iuneq2dv 5011	. 2 ⊢ (𝐺 Fn 𝐵 → ∪ 𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)})) = ∪ 𝑦 ∈ 𝐵 (◡(2nd ↾ (V × V)) ∘ ((◡(2nd ↾ (V × V)) “ {𝑦}) × (𝐺 “ {𝑦}))))
48	1, 7, 47	3eqtr4a 2790	1 ⊢ (𝐺 Fn 𝐵 → (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))) = ∪ 𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)})))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1533   ∈ wcel 2098   ≠ wne 2932  Vcvv 3466   ∩ cin 3939   ⊆ wss 3940  ∅c0 4314  {csn 4620  ∪ ciun 4987   × cxp 5664  ^◡ccnv 5665  dom cdm 5666  ran crn 5667   ↾ cres 5668   “ cima 5669   ∘ ccom 5670   Fn wfn 6528  ‘cfv 6533  2^nd c2nd 7967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-un 7718

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-1st 7968  df-2nd 7969

This theorem is referenced by:  fpar  8096