fparlem3

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

		Ref	Expression
	Assertion	fparlem3	⊢ ( 𝐹 Fn 𝐴 → ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( 𝐹 ∘ ( 1^st ↾ ( V × V ) ) ) ) = ∪ 𝑥 ∈ 𝐴 ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) ) )

Proof

Step	Hyp	Ref	Expression
1		coiun	⊢ ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ∪ 𝑥 ∈ 𝐴 ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) × ( 𝐹 “ { 𝑥 } ) ) ) = ∪ 𝑥 ∈ 𝐴 ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) × ( 𝐹 “ { 𝑥 } ) ) )
2		inss1	⊢ ( dom 𝐹 ∩ ran ( 1^st ↾ ( V × V ) ) ) ⊆ dom 𝐹
3		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
4	2 3	sseqtrid	⊢ ( 𝐹 Fn 𝐴 → ( dom 𝐹 ∩ ran ( 1^st ↾ ( V × V ) ) ) ⊆ 𝐴 )
5		dfco2a	⊢ ( ( dom 𝐹 ∩ ran ( 1^st ↾ ( V × V ) ) ) ⊆ 𝐴 → ( 𝐹 ∘ ( 1^st ↾ ( V × V ) ) ) = ∪ 𝑥 ∈ 𝐴 ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) × ( 𝐹 “ { 𝑥 } ) ) )
6	4 5	syl	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ∘ ( 1^st ↾ ( V × V ) ) ) = ∪ 𝑥 ∈ 𝐴 ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) × ( 𝐹 “ { 𝑥 } ) ) )
7	6	coeq2d	⊢ ( 𝐹 Fn 𝐴 → ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( 𝐹 ∘ ( 1^st ↾ ( V × V ) ) ) ) = ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ∪ 𝑥 ∈ 𝐴 ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) × ( 𝐹 “ { 𝑥 } ) ) ) )
8		inss1	⊢ ( dom ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ∩ ran ( 1^st ↾ ( V × V ) ) ) ⊆ dom ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) )
9		dmxpss	⊢ dom ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ⊆ { ( 𝐹 ‘ 𝑥 ) }
10	8 9	sstri	⊢ ( dom ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ∩ ran ( 1^st ↾ ( V × V ) ) ) ⊆ { ( 𝐹 ‘ 𝑥 ) }
11		dfco2a	⊢ ( ( dom ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ∩ ran ( 1^st ↾ ( V × V ) ) ) ⊆ { ( 𝐹 ‘ 𝑥 ) } → ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ∘ ( 1^st ↾ ( V × V ) ) ) = ∪ 𝑦 ∈ { ( 𝐹 ‘ 𝑥 ) } ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑦 } ) × ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) “ { 𝑦 } ) ) )
12	10 11	ax-mp	⊢ ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ∘ ( 1^st ↾ ( V × V ) ) ) = ∪ 𝑦 ∈ { ( 𝐹 ‘ 𝑥 ) } ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑦 } ) × ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) “ { 𝑦 } ) )
13		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
14		fparlem1	⊢ ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑦 } ) = ( { 𝑦 } × V )
15		sneq	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → { 𝑦 } = { ( 𝐹 ‘ 𝑥 ) } )
16	15	xpeq1d	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( { 𝑦 } × V ) = ( { ( 𝐹 ‘ 𝑥 ) } × V ) )
17	14 16	syl5eq	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑦 } ) = ( { ( 𝐹 ‘ 𝑥 ) } × V ) )
18	15	imaeq2d	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) “ { 𝑦 } ) = ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) “ { ( 𝐹 ‘ 𝑥 ) } ) )
19		df-ima	⊢ ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) “ { ( 𝐹 ‘ 𝑥 ) } ) = ran ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ↾ { ( 𝐹 ‘ 𝑥 ) } )
20		ssid	⊢ { ( 𝐹 ‘ 𝑥 ) } ⊆ { ( 𝐹 ‘ 𝑥 ) }
21		xpssres	⊢ ( { ( 𝐹 ‘ 𝑥 ) } ⊆ { ( 𝐹 ‘ 𝑥 ) } → ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ↾ { ( 𝐹 ‘ 𝑥 ) } ) = ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) )
22	20 21	ax-mp	⊢ ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ↾ { ( 𝐹 ‘ 𝑥 ) } ) = ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) )
23	22	rneqi	⊢ ran ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ↾ { ( 𝐹 ‘ 𝑥 ) } ) = ran ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) )
24	13	snnz	⊢ { ( 𝐹 ‘ 𝑥 ) } ≠ ∅
25		rnxp	⊢ ( { ( 𝐹 ‘ 𝑥 ) } ≠ ∅ → ran ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) = ( { 𝑥 } × V ) )
26	24 25	ax-mp	⊢ ran ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) = ( { 𝑥 } × V )
27	23 26	eqtri	⊢ ran ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ↾ { ( 𝐹 ‘ 𝑥 ) } ) = ( { 𝑥 } × V )
28	19 27	eqtri	⊢ ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) “ { ( 𝐹 ‘ 𝑥 ) } ) = ( { 𝑥 } × V )
29	18 28	syl6eq	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) “ { 𝑦 } ) = ( { 𝑥 } × V ) )
30	17 29	xpeq12d	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑦 } ) × ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) “ { 𝑦 } ) ) = ( ( { ( 𝐹 ‘ 𝑥 ) } × V ) × ( { 𝑥 } × V ) ) )
31	13 30	iunxsn	⊢ ∪ 𝑦 ∈ { ( 𝐹 ‘ 𝑥 ) } ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑦 } ) × ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) “ { 𝑦 } ) ) = ( ( { ( 𝐹 ‘ 𝑥 ) } × V ) × ( { 𝑥 } × V ) )
32	12 31	eqtri	⊢ ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ∘ ( 1^st ↾ ( V × V ) ) ) = ( ( { ( 𝐹 ‘ 𝑥 ) } × V ) × ( { 𝑥 } × V ) )
33	32	cnveqi	⊢ ^◡ ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ∘ ( 1^st ↾ ( V × V ) ) ) = ^◡ ( ( { ( 𝐹 ‘ 𝑥 ) } × V ) × ( { 𝑥 } × V ) )
34		cnvco	⊢ ^◡ ( ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ∘ ( 1^st ↾ ( V × V ) ) ) = ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ^◡ ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) )
35		cnvxp	⊢ ^◡ ( ( { ( 𝐹 ‘ 𝑥 ) } × V ) × ( { 𝑥 } × V ) ) = ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) )
36	33 34 35	3eqtr3i	⊢ ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ^◡ ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ) = ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) )
37		fparlem1	⊢ ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) = ( { 𝑥 } × V )
38	37	xpeq2i	⊢ ( { ( 𝐹 ‘ 𝑥 ) } × ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) ) = ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) )
39		fnsnfv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → { ( 𝐹 ‘ 𝑥 ) } = ( 𝐹 “ { 𝑥 } ) )
40	39	xpeq1d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( { ( 𝐹 ‘ 𝑥 ) } × ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) ) = ( ( 𝐹 “ { 𝑥 } ) × ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) ) )
41	38 40	syl5eqr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) = ( ( 𝐹 “ { 𝑥 } ) × ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) ) )
42	41	cnveqd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ^◡ ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) = ^◡ ( ( 𝐹 “ { 𝑥 } ) × ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) ) )
43		cnvxp	⊢ ^◡ ( ( 𝐹 “ { 𝑥 } ) × ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) ) = ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) × ( 𝐹 “ { 𝑥 } ) )
44	42 43	syl6eq	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ^◡ ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) = ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) × ( 𝐹 “ { 𝑥 } ) ) )
45	44	coeq2d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ^◡ ( { ( 𝐹 ‘ 𝑥 ) } × ( { 𝑥 } × V ) ) ) = ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) × ( 𝐹 “ { 𝑥 } ) ) ) )
46	36 45	syl5eqr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) ) = ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) × ( 𝐹 “ { 𝑥 } ) ) ) )
47	46	iuneq2dv	⊢ ( 𝐹 Fn 𝐴 → ∪ 𝑥 ∈ 𝐴 ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) ) = ∪ 𝑥 ∈ 𝐴 ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) × ( 𝐹 “ { 𝑥 } ) ) ) )
48	1 7 47	3eqtr4a	⊢ ( 𝐹 Fn 𝐴 → ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( 𝐹 ∘ ( 1^st ↾ ( V × V ) ) ) ) = ∪ 𝑥 ∈ 𝐴 ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) ) )

Metamath Proof Explorer

Theorem fparlem3

Proof