Step |
Hyp |
Ref |
Expression |
1 |
|
yoneda.y |
⊢ 𝑌 = ( Yon ‘ 𝐶 ) |
2 |
|
yoneda.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
3 |
|
yoneda.1 |
⊢ 1 = ( Id ‘ 𝐶 ) |
4 |
|
yoneda.o |
⊢ 𝑂 = ( oppCat ‘ 𝐶 ) |
5 |
|
yoneda.s |
⊢ 𝑆 = ( SetCat ‘ 𝑈 ) |
6 |
|
yoneda.t |
⊢ 𝑇 = ( SetCat ‘ 𝑉 ) |
7 |
|
yoneda.q |
⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 ) |
8 |
|
yoneda.h |
⊢ 𝐻 = ( HomF ‘ 𝑄 ) |
9 |
|
yoneda.r |
⊢ 𝑅 = ( ( 𝑄 ×c 𝑂 ) FuncCat 𝑇 ) |
10 |
|
yoneda.e |
⊢ 𝐸 = ( 𝑂 evalF 𝑆 ) |
11 |
|
yoneda.z |
⊢ 𝑍 = ( 𝐻 ∘func ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) ) |
12 |
|
yoneda.c |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
13 |
|
yoneda.w |
⊢ ( 𝜑 → 𝑉 ∈ 𝑊 ) |
14 |
|
yoneda.u |
⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 ) |
15 |
|
yoneda.v |
⊢ ( 𝜑 → ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 ) |
16 |
|
yoneda.m |
⊢ 𝑀 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑎 ∈ ( ( ( 1st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) ) ) |
17 |
|
ovex |
⊢ ( ( ( 1st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ∈ V |
18 |
17
|
mptex |
⊢ ( 𝑎 ∈ ( ( ( 1st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) ) ∈ V |
19 |
16 18
|
fnmpoi |
⊢ 𝑀 Fn ( ( 𝑂 Func 𝑆 ) × 𝐵 ) |
20 |
19
|
a1i |
⊢ ( 𝜑 → 𝑀 Fn ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ) |
21 |
12
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ Cat ) |
22 |
13
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝑉 ∈ 𝑊 ) |
23 |
14
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 ) |
24 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 ) |
25 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝑔 ∈ ( 𝑂 Func 𝑆 ) ) |
26 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 ) |
27 |
1 2 3 4 5 6 7 8 9 10 11 21 22 23 24 25 26 16
|
yonedalem3a |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑔 𝑀 𝑦 ) = ( 𝑎 ∈ ( ( ( 1st ‘ 𝑌 ) ‘ 𝑦 ) ( 𝑂 Nat 𝑆 ) 𝑔 ) ↦ ( ( 𝑎 ‘ 𝑦 ) ‘ ( 1 ‘ 𝑦 ) ) ) ∧ ( 𝑔 𝑀 𝑦 ) : ( 𝑔 ( 1st ‘ 𝑍 ) 𝑦 ) ⟶ ( 𝑔 ( 1st ‘ 𝐸 ) 𝑦 ) ) ) |
28 |
27
|
simprd |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑔 𝑀 𝑦 ) : ( 𝑔 ( 1st ‘ 𝑍 ) 𝑦 ) ⟶ ( 𝑔 ( 1st ‘ 𝐸 ) 𝑦 ) ) |
29 |
|
eqid |
⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 ) |
30 |
|
eqid |
⊢ ( 𝑄 ×c 𝑂 ) = ( 𝑄 ×c 𝑂 ) |
31 |
7
|
fucbas |
⊢ ( 𝑂 Func 𝑆 ) = ( Base ‘ 𝑄 ) |
32 |
4 2
|
oppcbas |
⊢ 𝐵 = ( Base ‘ 𝑂 ) |
33 |
30 31 32
|
xpcbas |
⊢ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) = ( Base ‘ ( 𝑄 ×c 𝑂 ) ) |
34 |
|
eqid |
⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 ) |
35 |
|
relfunc |
⊢ Rel ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) |
36 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
|
yonedalem1 |
⊢ ( 𝜑 → ( 𝑍 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ∧ 𝐸 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ) ) |
37 |
36
|
simpld |
⊢ ( 𝜑 → 𝑍 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ) |
38 |
|
1st2ndbr |
⊢ ( ( Rel ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ∧ 𝑍 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ) → ( 1st ‘ 𝑍 ) ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ( 2nd ‘ 𝑍 ) ) |
39 |
35 37 38
|
sylancr |
⊢ ( 𝜑 → ( 1st ‘ 𝑍 ) ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ( 2nd ‘ 𝑍 ) ) |
40 |
33 34 39
|
funcf1 |
⊢ ( 𝜑 → ( 1st ‘ 𝑍 ) : ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ⟶ ( Base ‘ 𝑇 ) ) |
41 |
40
|
fovrnda |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑔 ( 1st ‘ 𝑍 ) 𝑦 ) ∈ ( Base ‘ 𝑇 ) ) |
42 |
6 22
|
setcbas |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝑉 = ( Base ‘ 𝑇 ) ) |
43 |
41 42
|
eleqtrrd |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑔 ( 1st ‘ 𝑍 ) 𝑦 ) ∈ 𝑉 ) |
44 |
36
|
simprd |
⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ) |
45 |
|
1st2ndbr |
⊢ ( ( Rel ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ∧ 𝐸 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ) → ( 1st ‘ 𝐸 ) ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ( 2nd ‘ 𝐸 ) ) |
46 |
35 44 45
|
sylancr |
⊢ ( 𝜑 → ( 1st ‘ 𝐸 ) ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ( 2nd ‘ 𝐸 ) ) |
47 |
33 34 46
|
funcf1 |
⊢ ( 𝜑 → ( 1st ‘ 𝐸 ) : ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ⟶ ( Base ‘ 𝑇 ) ) |
48 |
47
|
fovrnda |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑔 ( 1st ‘ 𝐸 ) 𝑦 ) ∈ ( Base ‘ 𝑇 ) ) |
49 |
48 42
|
eleqtrrd |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑔 ( 1st ‘ 𝐸 ) 𝑦 ) ∈ 𝑉 ) |
50 |
6 22 29 43 49
|
elsetchom |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑔 𝑀 𝑦 ) ∈ ( ( 𝑔 ( 1st ‘ 𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1st ‘ 𝐸 ) 𝑦 ) ) ↔ ( 𝑔 𝑀 𝑦 ) : ( 𝑔 ( 1st ‘ 𝑍 ) 𝑦 ) ⟶ ( 𝑔 ( 1st ‘ 𝐸 ) 𝑦 ) ) ) |
51 |
28 50
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑔 𝑀 𝑦 ) ∈ ( ( 𝑔 ( 1st ‘ 𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1st ‘ 𝐸 ) 𝑦 ) ) ) |
52 |
51
|
ralrimivva |
⊢ ( 𝜑 → ∀ 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∀ 𝑦 ∈ 𝐵 ( 𝑔 𝑀 𝑦 ) ∈ ( ( 𝑔 ( 1st ‘ 𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1st ‘ 𝐸 ) 𝑦 ) ) ) |
53 |
|
fveq2 |
⊢ ( 𝑧 = 〈 𝑔 , 𝑦 〉 → ( 𝑀 ‘ 𝑧 ) = ( 𝑀 ‘ 〈 𝑔 , 𝑦 〉 ) ) |
54 |
|
df-ov |
⊢ ( 𝑔 𝑀 𝑦 ) = ( 𝑀 ‘ 〈 𝑔 , 𝑦 〉 ) |
55 |
53 54
|
eqtr4di |
⊢ ( 𝑧 = 〈 𝑔 , 𝑦 〉 → ( 𝑀 ‘ 𝑧 ) = ( 𝑔 𝑀 𝑦 ) ) |
56 |
|
fveq2 |
⊢ ( 𝑧 = 〈 𝑔 , 𝑦 〉 → ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) = ( ( 1st ‘ 𝑍 ) ‘ 〈 𝑔 , 𝑦 〉 ) ) |
57 |
|
df-ov |
⊢ ( 𝑔 ( 1st ‘ 𝑍 ) 𝑦 ) = ( ( 1st ‘ 𝑍 ) ‘ 〈 𝑔 , 𝑦 〉 ) |
58 |
56 57
|
eqtr4di |
⊢ ( 𝑧 = 〈 𝑔 , 𝑦 〉 → ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) = ( 𝑔 ( 1st ‘ 𝑍 ) 𝑦 ) ) |
59 |
|
fveq2 |
⊢ ( 𝑧 = 〈 𝑔 , 𝑦 〉 → ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) = ( ( 1st ‘ 𝐸 ) ‘ 〈 𝑔 , 𝑦 〉 ) ) |
60 |
|
df-ov |
⊢ ( 𝑔 ( 1st ‘ 𝐸 ) 𝑦 ) = ( ( 1st ‘ 𝐸 ) ‘ 〈 𝑔 , 𝑦 〉 ) |
61 |
59 60
|
eqtr4di |
⊢ ( 𝑧 = 〈 𝑔 , 𝑦 〉 → ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) = ( 𝑔 ( 1st ‘ 𝐸 ) 𝑦 ) ) |
62 |
58 61
|
oveq12d |
⊢ ( 𝑧 = 〈 𝑔 , 𝑦 〉 → ( ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) ) = ( ( 𝑔 ( 1st ‘ 𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1st ‘ 𝐸 ) 𝑦 ) ) ) |
63 |
55 62
|
eleq12d |
⊢ ( 𝑧 = 〈 𝑔 , 𝑦 〉 → ( ( 𝑀 ‘ 𝑧 ) ∈ ( ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) ) ↔ ( 𝑔 𝑀 𝑦 ) ∈ ( ( 𝑔 ( 1st ‘ 𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1st ‘ 𝐸 ) 𝑦 ) ) ) ) |
64 |
63
|
ralxp |
⊢ ( ∀ 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( 𝑀 ‘ 𝑧 ) ∈ ( ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) ) ↔ ∀ 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∀ 𝑦 ∈ 𝐵 ( 𝑔 𝑀 𝑦 ) ∈ ( ( 𝑔 ( 1st ‘ 𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1st ‘ 𝐸 ) 𝑦 ) ) ) |
65 |
52 64
|
sylibr |
⊢ ( 𝜑 → ∀ 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( 𝑀 ‘ 𝑧 ) ∈ ( ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) ) ) |
66 |
|
ovex |
⊢ ( 𝑂 Func 𝑆 ) ∈ V |
67 |
2
|
fvexi |
⊢ 𝐵 ∈ V |
68 |
66 67
|
mpoex |
⊢ ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑎 ∈ ( ( ( 1st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) ) ) ∈ V |
69 |
16 68
|
eqeltri |
⊢ 𝑀 ∈ V |
70 |
69
|
elixp |
⊢ ( 𝑀 ∈ X 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) ) ↔ ( 𝑀 Fn ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ ∀ 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( 𝑀 ‘ 𝑧 ) ∈ ( ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) ) ) ) |
71 |
20 65 70
|
sylanbrc |
⊢ ( 𝜑 → 𝑀 ∈ X 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) ) ) |
72 |
12
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝐶 ∈ Cat ) |
73 |
13
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑉 ∈ 𝑊 ) |
74 |
14
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 ) |
75 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 ) |
76 |
|
simpr1 |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ) |
77 |
|
xp1st |
⊢ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → ( 1st ‘ 𝑧 ) ∈ ( 𝑂 Func 𝑆 ) ) |
78 |
76 77
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 1st ‘ 𝑧 ) ∈ ( 𝑂 Func 𝑆 ) ) |
79 |
|
xp2nd |
⊢ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) |
80 |
76 79
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) |
81 |
|
simpr2 |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ) |
82 |
|
xp1st |
⊢ ( 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → ( 1st ‘ 𝑤 ) ∈ ( 𝑂 Func 𝑆 ) ) |
83 |
81 82
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 1st ‘ 𝑤 ) ∈ ( 𝑂 Func 𝑆 ) ) |
84 |
|
xp2nd |
⊢ ( 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → ( 2nd ‘ 𝑤 ) ∈ 𝐵 ) |
85 |
81 84
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 2nd ‘ 𝑤 ) ∈ 𝐵 ) |
86 |
|
simpr3 |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) |
87 |
|
eqid |
⊢ ( 𝑂 Nat 𝑆 ) = ( 𝑂 Nat 𝑆 ) |
88 |
7 87
|
fuchom |
⊢ ( 𝑂 Nat 𝑆 ) = ( Hom ‘ 𝑄 ) |
89 |
|
eqid |
⊢ ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 ) |
90 |
|
eqid |
⊢ ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) = ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) |
91 |
30 33 88 89 90 76 81
|
xpchom |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) = ( ( ( 1st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st ‘ 𝑤 ) ) × ( ( 2nd ‘ 𝑧 ) ( Hom ‘ 𝑂 ) ( 2nd ‘ 𝑤 ) ) ) ) |
92 |
|
eqid |
⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) |
93 |
92 4
|
oppchom |
⊢ ( ( 2nd ‘ 𝑧 ) ( Hom ‘ 𝑂 ) ( 2nd ‘ 𝑤 ) ) = ( ( 2nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd ‘ 𝑧 ) ) |
94 |
93
|
xpeq2i |
⊢ ( ( ( 1st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st ‘ 𝑤 ) ) × ( ( 2nd ‘ 𝑧 ) ( Hom ‘ 𝑂 ) ( 2nd ‘ 𝑤 ) ) ) = ( ( ( 1st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st ‘ 𝑤 ) ) × ( ( 2nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd ‘ 𝑧 ) ) ) |
95 |
91 94
|
eqtrdi |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) = ( ( ( 1st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st ‘ 𝑤 ) ) × ( ( 2nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd ‘ 𝑧 ) ) ) ) |
96 |
86 95
|
eleqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑔 ∈ ( ( ( 1st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st ‘ 𝑤 ) ) × ( ( 2nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd ‘ 𝑧 ) ) ) ) |
97 |
|
xp1st |
⊢ ( 𝑔 ∈ ( ( ( 1st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st ‘ 𝑤 ) ) × ( ( 2nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd ‘ 𝑧 ) ) ) → ( 1st ‘ 𝑔 ) ∈ ( ( 1st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st ‘ 𝑤 ) ) ) |
98 |
96 97
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 1st ‘ 𝑔 ) ∈ ( ( 1st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st ‘ 𝑤 ) ) ) |
99 |
|
xp2nd |
⊢ ( 𝑔 ∈ ( ( ( 1st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st ‘ 𝑤 ) ) × ( ( 2nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd ‘ 𝑧 ) ) ) → ( 2nd ‘ 𝑔 ) ∈ ( ( 2nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd ‘ 𝑧 ) ) ) |
100 |
96 99
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 2nd ‘ 𝑔 ) ∈ ( ( 2nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd ‘ 𝑧 ) ) ) |
101 |
1 2 3 4 5 6 7 8 9 10 11 72 73 74 75 78 80 83 85 98 100 16
|
yonedalem3b |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( ( 1st ‘ 𝑤 ) 𝑀 ( 2nd ‘ 𝑤 ) ) ( 〈 ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑧 ) ) , ( ( 1st ‘ 𝑤 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑤 ) ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝑤 ) ( 1st ‘ 𝐸 ) ( 2nd ‘ 𝑤 ) ) ) ( ( 1st ‘ 𝑔 ) ( 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ( 2nd ‘ 𝑍 ) 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ( 2nd ‘ 𝑔 ) ) ) = ( ( ( 1st ‘ 𝑔 ) ( 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ( 2nd ‘ 𝐸 ) 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ( 2nd ‘ 𝑔 ) ) ( 〈 ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑧 ) ) , ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝐸 ) ( 2nd ‘ 𝑧 ) ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝑤 ) ( 1st ‘ 𝐸 ) ( 2nd ‘ 𝑤 ) ) ) ( ( 1st ‘ 𝑧 ) 𝑀 ( 2nd ‘ 𝑧 ) ) ) ) |
102 |
|
1st2nd2 |
⊢ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → 𝑧 = 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ) |
103 |
76 102
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑧 = 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ) |
104 |
103
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) = ( ( 1st ‘ 𝑍 ) ‘ 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ) ) |
105 |
|
df-ov |
⊢ ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑍 ) ‘ 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ) |
106 |
104 105
|
eqtr4di |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) = ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑧 ) ) ) |
107 |
|
1st2nd2 |
⊢ ( 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → 𝑤 = 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) |
108 |
81 107
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑤 = 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) |
109 |
108
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st ‘ 𝑍 ) ‘ 𝑤 ) = ( ( 1st ‘ 𝑍 ) ‘ 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ) |
110 |
|
df-ov |
⊢ ( ( 1st ‘ 𝑤 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑤 ) ) = ( ( 1st ‘ 𝑍 ) ‘ 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) |
111 |
109 110
|
eqtr4di |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st ‘ 𝑍 ) ‘ 𝑤 ) = ( ( 1st ‘ 𝑤 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑤 ) ) ) |
112 |
106 111
|
opeq12d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 〈 ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝑍 ) ‘ 𝑤 ) 〉 = 〈 ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑧 ) ) , ( ( 1st ‘ 𝑤 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑤 ) ) 〉 ) |
113 |
108
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st ‘ 𝐸 ) ‘ 𝑤 ) = ( ( 1st ‘ 𝐸 ) ‘ 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ) |
114 |
|
df-ov |
⊢ ( ( 1st ‘ 𝑤 ) ( 1st ‘ 𝐸 ) ( 2nd ‘ 𝑤 ) ) = ( ( 1st ‘ 𝐸 ) ‘ 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) |
115 |
113 114
|
eqtr4di |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st ‘ 𝐸 ) ‘ 𝑤 ) = ( ( 1st ‘ 𝑤 ) ( 1st ‘ 𝐸 ) ( 2nd ‘ 𝑤 ) ) ) |
116 |
112 115
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 〈 ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝑍 ) ‘ 𝑤 ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑤 ) ) = ( 〈 ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑧 ) ) , ( ( 1st ‘ 𝑤 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑤 ) ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝑤 ) ( 1st ‘ 𝐸 ) ( 2nd ‘ 𝑤 ) ) ) ) |
117 |
108
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑀 ‘ 𝑤 ) = ( 𝑀 ‘ 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ) |
118 |
|
df-ov |
⊢ ( ( 1st ‘ 𝑤 ) 𝑀 ( 2nd ‘ 𝑤 ) ) = ( 𝑀 ‘ 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) |
119 |
117 118
|
eqtr4di |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑀 ‘ 𝑤 ) = ( ( 1st ‘ 𝑤 ) 𝑀 ( 2nd ‘ 𝑤 ) ) ) |
120 |
103 108
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑧 ( 2nd ‘ 𝑍 ) 𝑤 ) = ( 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ( 2nd ‘ 𝑍 ) 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ) |
121 |
|
1st2nd2 |
⊢ ( 𝑔 ∈ ( ( ( 1st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st ‘ 𝑤 ) ) × ( ( 2nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd ‘ 𝑧 ) ) ) → 𝑔 = 〈 ( 1st ‘ 𝑔 ) , ( 2nd ‘ 𝑔 ) 〉 ) |
122 |
96 121
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑔 = 〈 ( 1st ‘ 𝑔 ) , ( 2nd ‘ 𝑔 ) 〉 ) |
123 |
120 122
|
fveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑧 ( 2nd ‘ 𝑍 ) 𝑤 ) ‘ 𝑔 ) = ( ( 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ( 2nd ‘ 𝑍 ) 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ‘ 〈 ( 1st ‘ 𝑔 ) , ( 2nd ‘ 𝑔 ) 〉 ) ) |
124 |
|
df-ov |
⊢ ( ( 1st ‘ 𝑔 ) ( 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ( 2nd ‘ 𝑍 ) 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ( 2nd ‘ 𝑔 ) ) = ( ( 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ( 2nd ‘ 𝑍 ) 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ‘ 〈 ( 1st ‘ 𝑔 ) , ( 2nd ‘ 𝑔 ) 〉 ) |
125 |
123 124
|
eqtr4di |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑧 ( 2nd ‘ 𝑍 ) 𝑤 ) ‘ 𝑔 ) = ( ( 1st ‘ 𝑔 ) ( 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ( 2nd ‘ 𝑍 ) 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ( 2nd ‘ 𝑔 ) ) ) |
126 |
116 119 125
|
oveq123d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑀 ‘ 𝑤 ) ( 〈 ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝑍 ) ‘ 𝑤 ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2nd ‘ 𝑍 ) 𝑤 ) ‘ 𝑔 ) ) = ( ( ( 1st ‘ 𝑤 ) 𝑀 ( 2nd ‘ 𝑤 ) ) ( 〈 ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑧 ) ) , ( ( 1st ‘ 𝑤 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑤 ) ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝑤 ) ( 1st ‘ 𝐸 ) ( 2nd ‘ 𝑤 ) ) ) ( ( 1st ‘ 𝑔 ) ( 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ( 2nd ‘ 𝑍 ) 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ( 2nd ‘ 𝑔 ) ) ) ) |
127 |
103
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) = ( ( 1st ‘ 𝐸 ) ‘ 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ) ) |
128 |
|
df-ov |
⊢ ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝐸 ) ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝐸 ) ‘ 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ) |
129 |
127 128
|
eqtr4di |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) = ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝐸 ) ( 2nd ‘ 𝑧 ) ) ) |
130 |
106 129
|
opeq12d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 〈 ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) 〉 = 〈 ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑧 ) ) , ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝐸 ) ( 2nd ‘ 𝑧 ) ) 〉 ) |
131 |
130 115
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 〈 ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑤 ) ) = ( 〈 ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑧 ) ) , ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝐸 ) ( 2nd ‘ 𝑧 ) ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝑤 ) ( 1st ‘ 𝐸 ) ( 2nd ‘ 𝑤 ) ) ) ) |
132 |
103 108
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑧 ( 2nd ‘ 𝐸 ) 𝑤 ) = ( 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ( 2nd ‘ 𝐸 ) 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ) |
133 |
132 122
|
fveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑧 ( 2nd ‘ 𝐸 ) 𝑤 ) ‘ 𝑔 ) = ( ( 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ( 2nd ‘ 𝐸 ) 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ‘ 〈 ( 1st ‘ 𝑔 ) , ( 2nd ‘ 𝑔 ) 〉 ) ) |
134 |
|
df-ov |
⊢ ( ( 1st ‘ 𝑔 ) ( 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ( 2nd ‘ 𝐸 ) 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ( 2nd ‘ 𝑔 ) ) = ( ( 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ( 2nd ‘ 𝐸 ) 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ‘ 〈 ( 1st ‘ 𝑔 ) , ( 2nd ‘ 𝑔 ) 〉 ) |
135 |
133 134
|
eqtr4di |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑧 ( 2nd ‘ 𝐸 ) 𝑤 ) ‘ 𝑔 ) = ( ( 1st ‘ 𝑔 ) ( 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ( 2nd ‘ 𝐸 ) 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ( 2nd ‘ 𝑔 ) ) ) |
136 |
103
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑀 ‘ 𝑧 ) = ( 𝑀 ‘ 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ) ) |
137 |
|
df-ov |
⊢ ( ( 1st ‘ 𝑧 ) 𝑀 ( 2nd ‘ 𝑧 ) ) = ( 𝑀 ‘ 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ) |
138 |
136 137
|
eqtr4di |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑀 ‘ 𝑧 ) = ( ( 1st ‘ 𝑧 ) 𝑀 ( 2nd ‘ 𝑧 ) ) ) |
139 |
131 135 138
|
oveq123d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( ( 𝑧 ( 2nd ‘ 𝐸 ) 𝑤 ) ‘ 𝑔 ) ( 〈 ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑤 ) ) ( 𝑀 ‘ 𝑧 ) ) = ( ( ( 1st ‘ 𝑔 ) ( 〈 ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) 〉 ( 2nd ‘ 𝐸 ) 〈 ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) 〉 ) ( 2nd ‘ 𝑔 ) ) ( 〈 ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝑍 ) ( 2nd ‘ 𝑧 ) ) , ( ( 1st ‘ 𝑧 ) ( 1st ‘ 𝐸 ) ( 2nd ‘ 𝑧 ) ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝑤 ) ( 1st ‘ 𝐸 ) ( 2nd ‘ 𝑤 ) ) ) ( ( 1st ‘ 𝑧 ) 𝑀 ( 2nd ‘ 𝑧 ) ) ) ) |
140 |
101 126 139
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑀 ‘ 𝑤 ) ( 〈 ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝑍 ) ‘ 𝑤 ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2nd ‘ 𝑍 ) 𝑤 ) ‘ 𝑔 ) ) = ( ( ( 𝑧 ( 2nd ‘ 𝐸 ) 𝑤 ) ‘ 𝑔 ) ( 〈 ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑤 ) ) ( 𝑀 ‘ 𝑧 ) ) ) |
141 |
140
|
ralrimivvva |
⊢ ( 𝜑 → ∀ 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∀ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∀ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ( ( 𝑀 ‘ 𝑤 ) ( 〈 ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝑍 ) ‘ 𝑤 ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2nd ‘ 𝑍 ) 𝑤 ) ‘ 𝑔 ) ) = ( ( ( 𝑧 ( 2nd ‘ 𝐸 ) 𝑤 ) ‘ 𝑔 ) ( 〈 ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑤 ) ) ( 𝑀 ‘ 𝑧 ) ) ) |
142 |
|
eqid |
⊢ ( ( 𝑄 ×c 𝑂 ) Nat 𝑇 ) = ( ( 𝑄 ×c 𝑂 ) Nat 𝑇 ) |
143 |
|
eqid |
⊢ ( comp ‘ 𝑇 ) = ( comp ‘ 𝑇 ) |
144 |
142 33 90 29 143 37 44
|
isnat2 |
⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝑍 ( ( 𝑄 ×c 𝑂 ) Nat 𝑇 ) 𝐸 ) ↔ ( 𝑀 ∈ X 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) ) ∧ ∀ 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∀ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∀ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ( ( 𝑀 ‘ 𝑤 ) ( 〈 ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝑍 ) ‘ 𝑤 ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2nd ‘ 𝑍 ) 𝑤 ) ‘ 𝑔 ) ) = ( ( ( 𝑧 ( 2nd ‘ 𝐸 ) 𝑤 ) ‘ 𝑔 ) ( 〈 ( ( 1st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝐸 ) ‘ 𝑧 ) 〉 ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝐸 ) ‘ 𝑤 ) ) ( 𝑀 ‘ 𝑧 ) ) ) ) ) |
145 |
71 141 144
|
mpbir2and |
⊢ ( 𝜑 → 𝑀 ∈ ( 𝑍 ( ( 𝑄 ×c 𝑂 ) Nat 𝑇 ) 𝐸 ) ) |