Step |
Hyp |
Ref |
Expression |
1 |
|
fuccat.q |
⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 ) |
2 |
|
fuccat.r |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
3 |
|
fuccat.s |
⊢ ( 𝜑 → 𝐷 ∈ Cat ) |
4 |
|
fuccatid.1 |
⊢ 1 = ( Id ‘ 𝐷 ) |
5 |
1
|
fucbas |
⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 ) |
6 |
5
|
a1i |
⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 ) ) |
7 |
|
eqid |
⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 ) |
8 |
1 7
|
fuchom |
⊢ ( 𝐶 Nat 𝐷 ) = ( Hom ‘ 𝑄 ) |
9 |
8
|
a1i |
⊢ ( 𝜑 → ( 𝐶 Nat 𝐷 ) = ( Hom ‘ 𝑄 ) ) |
10 |
|
eqidd |
⊢ ( 𝜑 → ( comp ‘ 𝑄 ) = ( comp ‘ 𝑄 ) ) |
11 |
1
|
ovexi |
⊢ 𝑄 ∈ V |
12 |
11
|
a1i |
⊢ ( 𝜑 → 𝑄 ∈ V ) |
13 |
|
biid |
⊢ ( ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ℎ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ) ) ↔ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ℎ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ) ) ) |
14 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) |
15 |
1 7 4 14
|
fucidcl |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1 ∘ ( 1st ‘ 𝑓 ) ) ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑓 ) ) |
16 |
|
eqid |
⊢ ( comp ‘ 𝑄 ) = ( comp ‘ 𝑄 ) |
17 |
|
simpr31 |
⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ℎ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ) ) ) → 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ) |
18 |
1 7 16 4 17
|
fuclid |
⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ℎ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ) ) ) → ( ( 1 ∘ ( 1st ‘ 𝑓 ) ) ( 〈 𝑒 , 𝑓 〉 ( comp ‘ 𝑄 ) 𝑓 ) 𝑟 ) = 𝑟 ) |
19 |
|
simpr32 |
⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ℎ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ) ) ) → 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) |
20 |
1 7 16 4 19
|
fucrid |
⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ℎ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ) ) ) → ( 𝑠 ( 〈 𝑓 , 𝑓 〉 ( comp ‘ 𝑄 ) 𝑔 ) ( 1 ∘ ( 1st ‘ 𝑓 ) ) ) = 𝑠 ) |
21 |
1 7 16 17 19
|
fuccocl |
⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ℎ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ) ) ) → ( 𝑠 ( 〈 𝑒 , 𝑓 〉 ( comp ‘ 𝑄 ) 𝑔 ) 𝑟 ) ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) |
22 |
|
simpr33 |
⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ℎ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ) ) ) → 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ) |
23 |
1 7 16 17 19 22
|
fucass |
⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ℎ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ) ) ) → ( ( 𝑡 ( 〈 𝑓 , 𝑔 〉 ( comp ‘ 𝑄 ) ℎ ) 𝑠 ) ( 〈 𝑒 , 𝑓 〉 ( comp ‘ 𝑄 ) ℎ ) 𝑟 ) = ( 𝑡 ( 〈 𝑒 , 𝑔 〉 ( comp ‘ 𝑄 ) ℎ ) ( 𝑠 ( 〈 𝑒 , 𝑓 〉 ( comp ‘ 𝑄 ) 𝑔 ) 𝑟 ) ) ) |
24 |
6 9 10 12 13 15 18 20 21 23
|
iscatd2 |
⊢ ( 𝜑 → ( 𝑄 ∈ Cat ∧ ( Id ‘ 𝑄 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 1 ∘ ( 1st ‘ 𝑓 ) ) ) ) ) |