Proof of Theorem iscatd
Step | Hyp | Ref
| Expression |
1 | | iscatd.1 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 1 ∈ (𝑥𝐻𝑥)) |
2 | | iscatd.2 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦𝐻𝑥))) → ( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓) |
3 | 2 | 3exp2 1355 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑓 ∈ (𝑦𝐻𝑥) → ( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓)))) |
4 | 3 | imp31 421 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑓 ∈ (𝑦𝐻𝑥) → ( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓)) |
5 | 4 | ralrimiv 3095 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓) |
6 | | iscatd.3 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑥𝐻𝑦))) → (𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓) |
7 | 6 | 3exp2 1355 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑓 ∈ (𝑥𝐻𝑦) → (𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓)))) |
8 | 7 | imp31 421 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑓 ∈ (𝑥𝐻𝑦) → (𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓)) |
9 | 8 | ralrimiv 3095 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓) |
10 | 5, 9 | jca 515 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓)) |
11 | 10 | ralrimiva 3096 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓)) |
12 | | oveq1 7177 |
. . . . . . . . . . 11
⊢ (𝑔 = 1 → (𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = ( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓)) |
13 | 12 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ (𝑔 = 1 → ((𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ↔ ( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓)) |
14 | 13 | ralbidv 3109 |
. . . . . . . . 9
⊢ (𝑔 = 1 → (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓)) |
15 | | oveq2 7178 |
. . . . . . . . . . 11
⊢ (𝑔 = 1 → (𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = (𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 )) |
16 | 15 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ (𝑔 = 1 → ((𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓 ↔ (𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓)) |
17 | 16 | ralbidv 3109 |
. . . . . . . . 9
⊢ (𝑔 = 1 → (∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓)) |
18 | 14, 17 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑔 = 1 → ((∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓))) |
19 | 18 | ralbidv 3109 |
. . . . . . 7
⊢ (𝑔 = 1 → (∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓))) |
20 | 19 | rspcev 3526 |
. . . . . 6
⊢ (( 1 ∈ (𝑥𝐻𝑥) ∧ ∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓)) → ∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)) |
21 | 1, 11, 20 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)) |
22 | | iscatd.4 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
23 | 22 | 3expia 1122 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))) |
24 | 23 | 3exp2 1355 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝐵 → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)))))) |
25 | 24 | imp43 431 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))) |
26 | | iscatd.5 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) |
27 | 26 | 3expa 1119 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) |
28 | 27 | 3exp2 1355 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑓 ∈ (𝑥𝐻𝑦) → (𝑔 ∈ (𝑦𝐻𝑧) → (𝑘 ∈ (𝑧𝐻𝑤) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))))) |
29 | 28 | imp32 422 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑘 ∈ (𝑧𝐻𝑤) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) |
30 | 29 | ralrimiv 3095 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) |
31 | 30 | ex 416 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) |
32 | 31 | expr 460 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))))) |
33 | 32 | expd 419 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑧 ∈ 𝐵 → (𝑤 ∈ 𝐵 → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))))) |
34 | 33 | expr 460 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝐵 → (𝑤 ∈ 𝐵 → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))))))) |
35 | 34 | imp42 430 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑤 ∈ 𝐵) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) |
36 | 35 | ralrimdva 3101 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) |
37 | 25, 36 | jcad 516 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))))) |
38 | 37 | ralrimivv 3102 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) |
39 | 38 | ralrimivva 3103 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) |
40 | 21, 39 | jca 515 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))))) |
41 | 40 | ralrimiva 3096 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))))) |
42 | | iscatd.b |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) |
43 | | iscatd.h |
. . . . . . 7
⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) |
44 | 43 | oveqd 7187 |
. . . . . 6
⊢ (𝜑 → (𝑥𝐻𝑥) = (𝑥(Hom ‘𝐶)𝑥)) |
45 | 43 | oveqd 7187 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦𝐻𝑥) = (𝑦(Hom ‘𝐶)𝑥)) |
46 | | iscatd.o |
. . . . . . . . . . . 12
⊢ (𝜑 → · = (comp‘𝐶)) |
47 | 46 | oveqd 7187 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈𝑦, 𝑥〉 · 𝑥) = (〈𝑦, 𝑥〉(comp‘𝐶)𝑥)) |
48 | 47 | oveqd 7187 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = (𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓)) |
49 | 48 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ↔ (𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓)) |
50 | 45, 49 | raleqbidv 3304 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓)) |
51 | 43 | oveqd 7187 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥𝐻𝑦) = (𝑥(Hom ‘𝐶)𝑦)) |
52 | 46 | oveqd 7187 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈𝑥, 𝑥〉 · 𝑦) = (〈𝑥, 𝑥〉(comp‘𝐶)𝑦)) |
53 | 52 | oveqd 7187 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = (𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔)) |
54 | 53 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓 ↔ (𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓)) |
55 | 51, 54 | raleqbidv 3304 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓)) |
56 | 50, 55 | anbi12d 634 |
. . . . . . 7
⊢ (𝜑 → ((∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓))) |
57 | 42, 56 | raleqbidv 3304 |
. . . . . 6
⊢ (𝜑 → (∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓))) |
58 | 44, 57 | rexeqbidv 3305 |
. . . . 5
⊢ (𝜑 → (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ↔ ∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓))) |
59 | 43 | oveqd 7187 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦𝐻𝑧) = (𝑦(Hom ‘𝐶)𝑧)) |
60 | 46 | oveqd 7187 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈𝑥, 𝑦〉 · 𝑧) = (〈𝑥, 𝑦〉(comp‘𝐶)𝑧)) |
61 | 60 | oveqd 7187 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) |
62 | 43 | oveqd 7187 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥𝐻𝑧) = (𝑥(Hom ‘𝐶)𝑧)) |
63 | 61, 62 | eleq12d 2827 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) |
64 | 43 | oveqd 7187 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧𝐻𝑤) = (𝑧(Hom ‘𝐶)𝑤)) |
65 | 46 | oveqd 7187 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (〈𝑥, 𝑦〉 · 𝑤) = (〈𝑥, 𝑦〉(comp‘𝐶)𝑤)) |
66 | 46 | oveqd 7187 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (〈𝑦, 𝑧〉 · 𝑤) = (〈𝑦, 𝑧〉(comp‘𝐶)𝑤)) |
67 | 66 | oveqd 7187 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔) = (𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)) |
68 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑓 = 𝑓) |
69 | 65, 67, 68 | oveq123d 7191 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = ((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓)) |
70 | 46 | oveqd 7187 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (〈𝑥, 𝑧〉 · 𝑤) = (〈𝑥, 𝑧〉(comp‘𝐶)𝑤)) |
71 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑘 = 𝑘) |
72 | 70, 71, 61 | oveq123d 7191 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) |
73 | 69, 72 | eqeq12d 2754 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) ↔ ((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) |
74 | 64, 73 | raleqbidv 3304 |
. . . . . . . . . . 11
⊢ (𝜑 → (∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) ↔ ∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) |
75 | 42, 74 | raleqbidv 3304 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) |
76 | 63, 75 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
77 | 59, 76 | raleqbidv 3304 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
78 | 51, 77 | raleqbidv 3304 |
. . . . . . 7
⊢ (𝜑 → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
79 | 42, 78 | raleqbidv 3304 |
. . . . . 6
⊢ (𝜑 → (∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
80 | 42, 79 | raleqbidv 3304 |
. . . . 5
⊢ (𝜑 → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
81 | 58, 80 | anbi12d 634 |
. . . 4
⊢ (𝜑 → ((∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
82 | 42, 81 | raleqbidv 3304 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
83 | 41, 82 | mpbid 235 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
84 | | iscatd.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
85 | | eqid 2738 |
. . . 4
⊢
(Base‘𝐶) =
(Base‘𝐶) |
86 | | eqid 2738 |
. . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
87 | | eqid 2738 |
. . . 4
⊢
(comp‘𝐶) =
(comp‘𝐶) |
88 | 85, 86, 87 | iscat 17046 |
. . 3
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
89 | 84, 88 | syl 17 |
. 2
⊢ (𝜑 → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
90 | 83, 89 | mpbird 260 |
1
⊢ (𝜑 → 𝐶 ∈ Cat) |