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
|
syl5eqr |
⊢ ( ( ( 𝐹 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 𝐴 ) → ( 𝐻 ∘ 𝑆 ) = ( 𝑥 ∈ 𝐴 ↦ 〈 ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) 〉 ) ) |