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 417 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑓 ∈ (𝑦𝐻𝑥) → ( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓)) |
| 5 | 4 | ralrimiv 3145 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓) |
| 6 | | iscatd.3 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑥𝐻𝑦))) → (𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓) |
| 7 | 6 | 3exp2 1355 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑓 ∈ (𝑥𝐻𝑦) → (𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓)))) |
| 8 | 7 | imp31 417 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑓 ∈ (𝑥𝐻𝑦) → (𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓)) |
| 9 | 8 | ralrimiv 3145 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓) |
| 10 | 5, 9 | jca 511 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓)) |
| 11 | 10 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓)) |
| 12 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑔 = 1 → (𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = ( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓)) |
| 13 | 12 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑔 = 1 → ((𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ↔ ( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓)) |
| 14 | 13 | ralbidv 3178 |
. . . . . . . . 9
⊢ (𝑔 = 1 → (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓)) |
| 15 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑔 = 1 → (𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = (𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 )) |
| 16 | 15 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑔 = 1 → ((𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓 ↔ (𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓)) |
| 17 | 16 | ralbidv 3178 |
. . . . . . . . 9
⊢ (𝑔 = 1 → (∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓)) |
| 18 | 14, 17 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑔 = 1 → ((∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓))) |
| 19 | 18 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑔 = 1 → (∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓))) |
| 20 | 19 | rspcev 3622 |
. . . . . 6
⊢ (( 1 ∈ (𝑥𝐻𝑥) ∧ ∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓)) → ∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)) |
| 21 | 1, 11, 20 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)) |
| 22 | | iscatd.4 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
| 23 | 22 | 3expia 1122 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))) |
| 24 | 23 | 3exp2 1355 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝐵 → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)))))) |
| 25 | 24 | imp43 427 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))) |
| 26 | | iscatd.5 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) |
| 27 | 26 | 3expa 1119 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) |
| 28 | 27 | 3exp2 1355 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑓 ∈ (𝑥𝐻𝑦) → (𝑔 ∈ (𝑦𝐻𝑧) → (𝑘 ∈ (𝑧𝐻𝑤) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))))) |
| 29 | 28 | imp32 418 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑘 ∈ (𝑧𝐻𝑤) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) |
| 30 | 29 | ralrimiv 3145 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) |
| 31 | 30 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) |
| 32 | 31 | expr 456 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))))) |
| 33 | 32 | expd 415 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑧 ∈ 𝐵 → (𝑤 ∈ 𝐵 → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))))) |
| 34 | 33 | expr 456 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝐵 → (𝑤 ∈ 𝐵 → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))))))) |
| 35 | 34 | imp42 426 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑤 ∈ 𝐵) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) |
| 36 | 35 | ralrimdva 3154 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) |
| 37 | 25, 36 | jcad 512 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))))) |
| 38 | 37 | ralrimivv 3200 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) |
| 39 | 38 | ralrimivva 3202 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) |
| 40 | 21, 39 | jca 511 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))))) |
| 41 | 40 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))))) |
| 42 | | iscatd.b |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) |
| 43 | | iscatd.h |
. . . . . . 7
⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) |
| 44 | 43 | oveqd 7448 |
. . . . . 6
⊢ (𝜑 → (𝑥𝐻𝑥) = (𝑥(Hom ‘𝐶)𝑥)) |
| 45 | 43 | oveqd 7448 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦𝐻𝑥) = (𝑦(Hom ‘𝐶)𝑥)) |
| 46 | | iscatd.o |
. . . . . . . . . . . 12
⊢ (𝜑 → · = (comp‘𝐶)) |
| 47 | 46 | oveqd 7448 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈𝑦, 𝑥〉 · 𝑥) = (〈𝑦, 𝑥〉(comp‘𝐶)𝑥)) |
| 48 | 47 | oveqd 7448 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = (𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓)) |
| 49 | 48 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ↔ (𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓)) |
| 50 | 45, 49 | raleqbidv 3346 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓)) |
| 51 | 43 | oveqd 7448 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥𝐻𝑦) = (𝑥(Hom ‘𝐶)𝑦)) |
| 52 | 46 | oveqd 7448 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈𝑥, 𝑥〉 · 𝑦) = (〈𝑥, 𝑥〉(comp‘𝐶)𝑦)) |
| 53 | 52 | oveqd 7448 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = (𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔)) |
| 54 | 53 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓 ↔ (𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓)) |
| 55 | 51, 54 | raleqbidv 3346 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓)) |
| 56 | 50, 55 | anbi12d 632 |
. . . . . . 7
⊢ (𝜑 → ((∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓))) |
| 57 | 42, 56 | raleqbidv 3346 |
. . . . . 6
⊢ (𝜑 → (∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓))) |
| 58 | 44, 57 | rexeqbidv 3347 |
. . . . 5
⊢ (𝜑 → (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ↔ ∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓))) |
| 59 | 43 | oveqd 7448 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦𝐻𝑧) = (𝑦(Hom ‘𝐶)𝑧)) |
| 60 | 46 | oveqd 7448 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈𝑥, 𝑦〉 · 𝑧) = (〈𝑥, 𝑦〉(comp‘𝐶)𝑧)) |
| 61 | 60 | oveqd 7448 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) |
| 62 | 43 | oveqd 7448 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥𝐻𝑧) = (𝑥(Hom ‘𝐶)𝑧)) |
| 63 | 61, 62 | eleq12d 2835 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) |
| 64 | 43 | oveqd 7448 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧𝐻𝑤) = (𝑧(Hom ‘𝐶)𝑤)) |
| 65 | 46 | oveqd 7448 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (〈𝑥, 𝑦〉 · 𝑤) = (〈𝑥, 𝑦〉(comp‘𝐶)𝑤)) |
| 66 | 46 | oveqd 7448 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (〈𝑦, 𝑧〉 · 𝑤) = (〈𝑦, 𝑧〉(comp‘𝐶)𝑤)) |
| 67 | 66 | oveqd 7448 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔) = (𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)) |
| 68 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑓 = 𝑓) |
| 69 | 65, 67, 68 | oveq123d 7452 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = ((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓)) |
| 70 | 46 | oveqd 7448 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (〈𝑥, 𝑧〉 · 𝑤) = (〈𝑥, 𝑧〉(comp‘𝐶)𝑤)) |
| 71 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑘 = 𝑘) |
| 72 | 70, 71, 61 | oveq123d 7452 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) |
| 73 | 69, 72 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) ↔ ((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) |
| 74 | 64, 73 | raleqbidv 3346 |
. . . . . . . . . . 11
⊢ (𝜑 → (∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) ↔ ∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) |
| 75 | 42, 74 | raleqbidv 3346 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) |
| 76 | 63, 75 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
| 77 | 59, 76 | raleqbidv 3346 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
| 78 | 51, 77 | raleqbidv 3346 |
. . . . . . 7
⊢ (𝜑 → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
| 79 | 42, 78 | raleqbidv 3346 |
. . . . . 6
⊢ (𝜑 → (∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
| 80 | 42, 79 | raleqbidv 3346 |
. . . . 5
⊢ (𝜑 → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))))) |
| 81 | 58, 80 | anbi12d 632 |
. . . 4
⊢ (𝜑 → ((∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
| 82 | 42, 81 | raleqbidv 3346 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(〈𝑦, 𝑧〉(comp‘𝐶)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝐶)𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉(comp‘𝐶)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))))) |
| 83 | 41, 82 | mpbid 232 |
. 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 2737 |
. . . 4
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 86 | | eqid 2737 |
. . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 87 | | eqid 2737 |
. . . 4
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 88 | 85, 86, 87 | iscat 17715 |
. . 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 257 |
1
⊢ (𝜑 → 𝐶 ∈ Cat) |