This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fsplitfpar

Description: Merge two functions with a common argument in parallel. Combination of fsplit and fpar . (Contributed by AV, 3-Jan-2024)

Ref Expression
Hypotheses fsplitfpar.h ⊢ 𝐻 = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝐹 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝐺 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
fsplitfpar.s ⊢ 𝑆 = ( ◡ ( 1st ↾ I ) ↾ 𝐴 )
Assertion fsplitfpar ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐻 ∘ 𝑆 ) = ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) )

Proof

Step Hyp Ref Expression
1 fsplitfpar.h ⊢ 𝐻 = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝐹 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝐺 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
2 fsplitfpar.s ⊢ 𝑆 = ( ◡ ( 1st ↾ I ) ↾ 𝐴 )
3 fsplit ⊢ ◡ ( 1st ↾ I ) = ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ )
4 3 reseq1i ⊢ ( ◡ ( 1st ↾ I ) ↾ 𝐴 ) = ( ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ↾ 𝐴 )
5 2 4 eqtri ⊢ 𝑆 = ( ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ↾ 𝐴 )
6 5 fveq1i ⊢ ( 𝑆 ‘ 𝑎 ) = ( ( ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ↾ 𝐴 ) ‘ 𝑎 )
7 6 a1i ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑎 ) = ( ( ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ↾ 𝐴 ) ‘ 𝑎 ) )
8 fvres ⊢ ( 𝑎 ∈ 𝐴 → ( ( ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ↾ 𝐴 ) ‘ 𝑎 ) = ( ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ‘ 𝑎 ) )
9 eqidd ⊢ ( 𝑎 ∈ 𝐴 → ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ ) = ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ ) )
10 id ⊢ ( 𝑥 = 𝑎 → 𝑥 = 𝑎 )
11 10 10 opeq12d ⊢ ( 𝑥 = 𝑎 → ⟨ 𝑥 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑎 ⟩ )
12 11 adantl ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = 𝑎 ) → ⟨ 𝑥 , 𝑥 ⟩ = ⟨ 𝑎 , 𝑎 ⟩ )
13 elex ⊢ ( 𝑎 ∈ 𝐴 → 𝑎 ∈ V )
14 opex ⊢ ⟨ 𝑎 , 𝑎 ⟩ ∈ V
15 14 a1i ⊢ ( 𝑎 ∈ 𝐴 → ⟨ 𝑎 , 𝑎 ⟩ ∈ V )
16 9 12 13 15 fvmptd ⊢ ( 𝑎 ∈ 𝐴 → ( ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ‘ 𝑎 ) = ⟨ 𝑎 , 𝑎 ⟩ )
17 8 16 eqtrd ⊢ ( 𝑎 ∈ 𝐴 → ( ( ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ↾ 𝐴 ) ‘ 𝑎 ) = ⟨ 𝑎 , 𝑎 ⟩ )
18 17 adantl ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ↾ 𝐴 ) ‘ 𝑎 ) = ⟨ 𝑎 , 𝑎 ⟩ )
19 7 18 eqtrd ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑎 ) = ⟨ 𝑎 , 𝑎 ⟩ )
20 19 fveq2d ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐻 ‘ ( 𝑆 ‘ 𝑎 ) ) = ( 𝐻 ‘ ⟨ 𝑎 , 𝑎 ⟩ ) )
21 df-ov ⊢ ( 𝑎 𝐻 𝑎 ) = ( 𝐻 ‘ ⟨ 𝑎 , 𝑎 ⟩ )
22 1 fpar ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → 𝐻 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ) )
23 22 adantr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → 𝐻 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ) )
24 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑎 ) )
25 24 adantr ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑎 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑎 ) )
26 fveq2 ⊢ ( 𝑦 = 𝑎 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑎 ) )
27 26 adantl ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑎 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑎 ) )
28 25 27 opeq12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑎 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ )
29 28 adantl ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑎 ) ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ )
30 simpr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 )
31 opex ⊢ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ∈ V
32 31 a1i ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ∈ V )
33 23 29 30 30 32 ovmpod ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 𝐻 𝑎 ) = ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ )
34 21 33 eqtr3id ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐻 ‘ ⟨ 𝑎 , 𝑎 ⟩ ) = ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ )
35 20 34 eqtrd ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐻 ‘ ( 𝑆 ‘ 𝑎 ) ) = ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ )
36 eqid ⊢ ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) = ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ )
37 36 fnmpt ⊢ ( ∀ 𝑎 ∈ V ⟨ 𝑎 , 𝑎 ⟩ ∈ V → ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) Fn V )
38 14 a1i ⊢ ( 𝑎 ∈ V → ⟨ 𝑎 , 𝑎 ⟩ ∈ V )
39 37 38 mprg ⊢ ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) Fn V
40 ssv ⊢ 𝐴 ⊆ V
41 fnssres ⊢ ( ( ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) Fn V ∧ 𝐴 ⊆ V ) → ( ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) ↾ 𝐴 ) Fn 𝐴 )
42 39 40 41 mp2an ⊢ ( ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) ↾ 𝐴 ) Fn 𝐴
43 fsplit ⊢ ◡ ( 1st ↾ I ) = ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ )
44 43 reseq1i ⊢ ( ◡ ( 1st ↾ I ) ↾ 𝐴 ) = ( ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) ↾ 𝐴 )
45 2 44 eqtri ⊢ 𝑆 = ( ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) ↾ 𝐴 )
46 45 fneq1i ⊢ ( 𝑆 Fn 𝐴 ↔ ( ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) ↾ 𝐴 ) Fn 𝐴 )
47 42 46 mpbir ⊢ 𝑆 Fn 𝐴
48 47 a1i ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → 𝑆 Fn 𝐴 )
49 fvco2 ⊢ ( ( 𝑆 Fn 𝐴 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐻 ∘ 𝑆 ) ‘ 𝑎 ) = ( 𝐻 ‘ ( 𝑆 ‘ 𝑎 ) ) )
50 48 49 sylan ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐻 ∘ 𝑆 ) ‘ 𝑎 ) = ( 𝐻 ‘ ( 𝑆 ‘ 𝑎 ) ) )
51 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑎 ) )
52 24 51 opeq12d ⊢ ( 𝑥 = 𝑎 → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ )
53 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) = ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ )
54 52 53 31 fvmpt ⊢ ( 𝑎 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑎 ) = ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ )
55 54 adantl ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑎 ) = ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ )
56 35 50 55 3eqtr4d ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐻 ∘ 𝑆 ) ‘ 𝑎 ) = ( ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑎 ) )
57 56 ralrimiva ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ∀ 𝑎 ∈ 𝐴 ( ( 𝐻 ∘ 𝑆 ) ‘ 𝑎 ) = ( ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑎 ) )
58 opex ⊢ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ∈ V
59 58 a1i ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ∈ V )
60 59 ralrimivva ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ∈ V )
61 eqid ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ )
62 61 fnmpo ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ∈ V → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ) Fn ( 𝐴 × 𝐴 ) )
63 60 62 syl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ) Fn ( 𝐴 × 𝐴 ) )
64 22 fneq1d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐻 Fn ( 𝐴 × 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ) Fn ( 𝐴 × 𝐴 ) ) )
65 63 64 mpbird ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → 𝐻 Fn ( 𝐴 × 𝐴 ) )
66 14 a1i ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑎 ∈ V ) → ⟨ 𝑎 , 𝑎 ⟩ ∈ V )
67 66 ralrimiva ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ∀ 𝑎 ∈ V ⟨ 𝑎 , 𝑎 ⟩ ∈ V )
68 67 37 syl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) Fn V )
69 68 40 41 sylancl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) ↾ 𝐴 ) Fn 𝐴 )
70 69 46 sylibr ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → 𝑆 Fn 𝐴 )
71 45 rneqi ⊢ ran 𝑆 = ran ( ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) ↾ 𝐴 )
72 mptima ⊢ ( ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) “ 𝐴 ) = ran ( 𝑎 ∈ ( V ∩ 𝐴 ) ↦ ⟨ 𝑎 , 𝑎 ⟩ )
73 df-ima ⊢ ( ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) “ 𝐴 ) = ran ( ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) ↾ 𝐴 )
74 eqid ⊢ ( 𝑎 ∈ ( V ∩ 𝐴 ) ↦ ⟨ 𝑎 , 𝑎 ⟩ ) = ( 𝑎 ∈ ( V ∩ 𝐴 ) ↦ ⟨ 𝑎 , 𝑎 ⟩ )
75 74 rnmpt ⊢ ran ( 𝑎 ∈ ( V ∩ 𝐴 ) ↦ ⟨ 𝑎 , 𝑎 ⟩ ) = { 𝑝 ∣ ∃ 𝑎 ∈ ( V ∩ 𝐴 ) 𝑝 = ⟨ 𝑎 , 𝑎 ⟩ }
76 72 73 75 3eqtr3i ⊢ ran ( ( 𝑎 ∈ V ↦ ⟨ 𝑎 , 𝑎 ⟩ ) ↾ 𝐴 ) = { 𝑝 ∣ ∃ 𝑎 ∈ ( V ∩ 𝐴 ) 𝑝 = ⟨ 𝑎 , 𝑎 ⟩ }
77 71 76 eqtri ⊢ ran 𝑆 = { 𝑝 ∣ ∃ 𝑎 ∈ ( V ∩ 𝐴 ) 𝑝 = ⟨ 𝑎 , 𝑎 ⟩ }
78 elinel2 ⊢ ( 𝑎 ∈ ( V ∩ 𝐴 ) → 𝑎 ∈ 𝐴 )
79 simpl ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑝 = ⟨ 𝑎 , 𝑎 ⟩ ) → 𝑎 ∈ 𝐴 )
80 79 79 opelxpd ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑝 = ⟨ 𝑎 , 𝑎 ⟩ ) → ⟨ 𝑎 , 𝑎 ⟩ ∈ ( 𝐴 × 𝐴 ) )
81 eleq1 ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑎 ⟩ → ( 𝑝 ∈ ( 𝐴 × 𝐴 ) ↔ ⟨ 𝑎 , 𝑎 ⟩ ∈ ( 𝐴 × 𝐴 ) ) )
82 81 adantl ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑝 = ⟨ 𝑎 , 𝑎 ⟩ ) → ( 𝑝 ∈ ( 𝐴 × 𝐴 ) ↔ ⟨ 𝑎 , 𝑎 ⟩ ∈ ( 𝐴 × 𝐴 ) ) )
83 80 82 mpbird ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑝 = ⟨ 𝑎 , 𝑎 ⟩ ) → 𝑝 ∈ ( 𝐴 × 𝐴 ) )
84 83 ex ⊢ ( 𝑎 ∈ 𝐴 → ( 𝑝 = ⟨ 𝑎 , 𝑎 ⟩ → 𝑝 ∈ ( 𝐴 × 𝐴 ) ) )
85 78 84 syl ⊢ ( 𝑎 ∈ ( V ∩ 𝐴 ) → ( 𝑝 = ⟨ 𝑎 , 𝑎 ⟩ → 𝑝 ∈ ( 𝐴 × 𝐴 ) ) )
86 85 rexlimiv ⊢ ( ∃ 𝑎 ∈ ( V ∩ 𝐴 ) 𝑝 = ⟨ 𝑎 , 𝑎 ⟩ → 𝑝 ∈ ( 𝐴 × 𝐴 ) )
87 86 abssi ⊢ { 𝑝 ∣ ∃ 𝑎 ∈ ( V ∩ 𝐴 ) 𝑝 = ⟨ 𝑎 , 𝑎 ⟩ } ⊆ ( 𝐴 × 𝐴 )
88 87 a1i ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → { 𝑝 ∣ ∃ 𝑎 ∈ ( V ∩ 𝐴 ) 𝑝 = ⟨ 𝑎 , 𝑎 ⟩ } ⊆ ( 𝐴 × 𝐴 ) )
89 77 88 eqsstrid ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ran 𝑆 ⊆ ( 𝐴 × 𝐴 ) )
90 fnco ⊢ ( ( 𝐻 Fn ( 𝐴 × 𝐴 ) ∧ 𝑆 Fn 𝐴 ∧ ran 𝑆 ⊆ ( 𝐴 × 𝐴 ) ) → ( 𝐻 ∘ 𝑆 ) Fn 𝐴 )
91 65 70 89 90 syl3anc ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐻 ∘ 𝑆 ) Fn 𝐴 )
92 opex ⊢ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ V
93 92 a1i ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ V )
94 93 ralrimiva ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ∀ 𝑥 ∈ 𝐴 ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ V )
95 53 fnmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ V → ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) Fn 𝐴 )
96 94 95 syl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) Fn 𝐴 )
97 eqfnfv ⊢ ( ( ( 𝐻 ∘ 𝑆 ) Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) Fn 𝐴 ) → ( ( 𝐻 ∘ 𝑆 ) = ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ↔ ∀ 𝑎 ∈ 𝐴 ( ( 𝐻 ∘ 𝑆 ) ‘ 𝑎 ) = ( ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑎 ) ) )
98 91 96 97 syl2anc ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( ( 𝐻 ∘ 𝑆 ) = ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ↔ ∀ 𝑎 ∈ 𝐴 ( ( 𝐻 ∘ 𝑆 ) ‘ 𝑎 ) = ( ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑎 ) ) )
99 57 98 mpbird ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐻 ∘ 𝑆 ) = ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) )