Metamath Proof Explorer

Theorem fparlem4

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

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

Proof

Step Hyp Ref Expression
1 coiun ⊢ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ∪ 𝑦 ∈ 𝐵 ( ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) × ( 𝐺 “ { 𝑦 } ) ) ) = ∪ 𝑦 ∈ 𝐵 ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) × ( 𝐺 “ { 𝑦 } ) ) )
2 inss1 ⊢ ( dom 𝐺 ∩ ran ( 2nd ↾ ( V × V ) ) ) ⊆ dom 𝐺
3 fndm ⊢ ( 𝐺 Fn 𝐵 → dom 𝐺 = 𝐵 )
4 2 3 sseqtrid ⊢ ( 𝐺 Fn 𝐵 → ( dom 𝐺 ∩ ran ( 2nd ↾ ( V × V ) ) ) ⊆ 𝐵 )
5 dfco2a ⊢ ( ( dom 𝐺 ∩ ran ( 2nd ↾ ( V × V ) ) ) ⊆ 𝐵 → ( 𝐺 ∘ ( 2nd ↾ ( V × V ) ) ) = ∪ 𝑦 ∈ 𝐵 ( ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) × ( 𝐺 “ { 𝑦 } ) ) )
6 4 5 syl ⊢ ( 𝐺 Fn 𝐵 → ( 𝐺 ∘ ( 2nd ↾ ( V × V ) ) ) = ∪ 𝑦 ∈ 𝐵 ( ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) × ( 𝐺 “ { 𝑦 } ) ) )
7 6 coeq2d ⊢ ( 𝐺 Fn 𝐵 → ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝐺 ∘ ( 2nd ↾ ( V × V ) ) ) ) = ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ∪ 𝑦 ∈ 𝐵 ( ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) × ( 𝐺 “ { 𝑦 } ) ) ) )
8 inss1 ⊢ ( dom ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) ∩ ran ( 2nd ↾ ( V × V ) ) ) ⊆ dom ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) )
9 dmxpss ⊢ dom ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) ⊆ { ( 𝐺 ‘ 𝑦 ) }
10 8 9 sstri ⊢ ( dom ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) ∩ ran ( 2nd ↾ ( V × V ) ) ) ⊆ { ( 𝐺 ‘ 𝑦 ) }
11 dfco2a ⊢ ( ( dom ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) ∩ ran ( 2nd ↾ ( V × V ) ) ) ⊆ { ( 𝐺 ‘ 𝑦 ) } → ( ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) ∘ ( 2nd ↾ ( V × V ) ) ) = ∪ 𝑥 ∈ { ( 𝐺 ‘ 𝑦 ) } ( ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑥 } ) × ( ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) “ { 𝑥 } ) ) )
12 10 11 ax-mp ⊢ ( ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) ∘ ( 2nd ↾ ( V × V ) ) ) = ∪ 𝑥 ∈ { ( 𝐺 ‘ 𝑦 ) } ( ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑥 } ) × ( ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) “ { 𝑥 } ) )
13 fvex ⊢ ( 𝐺 ‘ 𝑦 ) ∈ V
14 fparlem2 ⊢ ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑥 } ) = ( V × { 𝑥 } )
15 sneq ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑦 ) → { 𝑥 } = { ( 𝐺 ‘ 𝑦 ) } )
16 15 xpeq2d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑦 ) → ( V × { 𝑥 } ) = ( V × { ( 𝐺 ‘ 𝑦 ) } ) )
17 14 16 eqtrid ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑦 ) → ( ◡ ( 2nd ↾ ( 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 eqtrdi ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑦 ) → ( ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) “ { 𝑥 } ) = ( V × { 𝑦 } ) )
30 17 29 xpeq12d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑦 ) → ( ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑥 } ) × ( ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) “ { 𝑥 } ) ) = ( ( V × { ( 𝐺 ‘ 𝑦 ) } ) × ( V × { 𝑦 } ) ) )
31 13 30 iunxsn ⊢ ∪ 𝑥 ∈ { ( 𝐺 ‘ 𝑦 ) } ( ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑥 } ) × ( ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) “ { 𝑥 } ) ) = ( ( V × { ( 𝐺 ‘ 𝑦 ) } ) × ( V × { 𝑦 } ) )
32 12 31 eqtri ⊢ ( ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) ∘ ( 2nd ↾ ( V × V ) ) ) = ( ( V × { ( 𝐺 ‘ 𝑦 ) } ) × ( V × { 𝑦 } ) )
33 32 cnveqi ⊢ ◡ ( ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) ∘ ( 2nd ↾ ( V × V ) ) ) = ◡ ( ( V × { ( 𝐺 ‘ 𝑦 ) } ) × ( V × { 𝑦 } ) )
34 cnvco ⊢ ◡ ( ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) ∘ ( 2nd ↾ ( V × V ) ) ) = ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ◡ ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) )
35 cnvxp ⊢ ◡ ( ( V × { ( 𝐺 ‘ 𝑦 ) } ) × ( V × { 𝑦 } ) ) = ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) )
36 33 34 35 3eqtr3i ⊢ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ◡ ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) ) = ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) )
37 fparlem2 ⊢ ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) = ( V × { 𝑦 } )
38 37 xpeq2i ⊢ ( { ( 𝐺 ‘ 𝑦 ) } × ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) ) = ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) )
39 fnsnfv ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵 ) → { ( 𝐺 ‘ 𝑦 ) } = ( 𝐺 “ { 𝑦 } ) )
40 39 xpeq1d ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( { ( 𝐺 ‘ 𝑦 ) } × ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) ) = ( ( 𝐺 “ { 𝑦 } ) × ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) ) )
41 38 40 eqtr3id ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) = ( ( 𝐺 “ { 𝑦 } ) × ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) ) )
42 41 cnveqd ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ◡ ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) = ◡ ( ( 𝐺 “ { 𝑦 } ) × ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) ) )
43 cnvxp ⊢ ◡ ( ( 𝐺 “ { 𝑦 } ) × ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) ) = ( ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) × ( 𝐺 “ { 𝑦 } ) )
44 42 43 eqtrdi ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ◡ ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) = ( ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) × ( 𝐺 “ { 𝑦 } ) ) )
45 44 coeq2d ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ◡ ( { ( 𝐺 ‘ 𝑦 ) } × ( V × { 𝑦 } ) ) ) = ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) × ( 𝐺 “ { 𝑦 } ) ) ) )
46 36 45 eqtr3id ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) = ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) × ( 𝐺 “ { 𝑦 } ) ) ) )
47 46 iuneq2dv ⊢ ( 𝐺 Fn 𝐵 → ∪ 𝑦 ∈ 𝐵 ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) = ∪ 𝑦 ∈ 𝐵 ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( ( ◡ ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) × ( 𝐺 “ { 𝑦 } ) ) ) )
48 1 7 47 3eqtr4a ⊢ ( 𝐺 Fn 𝐵 → ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝐺 ∘ ( 2nd ↾ ( V × V ) ) ) ) = ∪ 𝑦 ∈ 𝐵 ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) )