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 𝐴 ) → ( 𝐻𝑆 ) = ( 𝑥𝐴 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) )