| Step | Hyp | Ref
| Expression |
| 1 | | catcone0.f |
. . . 4
⊢ (𝜑 → (𝑋𝐻𝑌) ≠ ∅) |
| 2 | | catcone0.g |
. . . 4
⊢ (𝜑 → (𝑌𝐻𝑍) ≠ ∅) |
| 3 | | n0 4353 |
. . . . . 6
⊢ ((𝑋𝐻𝑌) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝑋𝐻𝑌)) |
| 4 | | n0 4353 |
. . . . . 6
⊢ ((𝑌𝐻𝑍) ≠ ∅ ↔ ∃𝑔 𝑔 ∈ (𝑌𝐻𝑍)) |
| 5 | 3, 4 | anbi12i 628 |
. . . . 5
⊢ (((𝑋𝐻𝑌) ≠ ∅ ∧ (𝑌𝐻𝑍) ≠ ∅) ↔ (∃𝑓 𝑓 ∈ (𝑋𝐻𝑌) ∧ ∃𝑔 𝑔 ∈ (𝑌𝐻𝑍))) |
| 6 | | exdistrv 1955 |
. . . . 5
⊢
(∃𝑓∃𝑔(𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍)) ↔ (∃𝑓 𝑓 ∈ (𝑋𝐻𝑌) ∧ ∃𝑔 𝑔 ∈ (𝑌𝐻𝑍))) |
| 7 | 5, 6 | sylbb2 238 |
. . . 4
⊢ (((𝑋𝐻𝑌) ≠ ∅ ∧ (𝑌𝐻𝑍) ≠ ∅) → ∃𝑓∃𝑔(𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) |
| 8 | 1, 2, 7 | syl2anc 584 |
. . 3
⊢ (𝜑 → ∃𝑓∃𝑔(𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) |
| 9 | 8 | ancli 548 |
. 2
⊢ (𝜑 → (𝜑 ∧ ∃𝑓∃𝑔(𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍)))) |
| 10 | | 19.42vv 1957 |
. . 3
⊢
(∃𝑓∃𝑔(𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) ↔ (𝜑 ∧ ∃𝑓∃𝑔(𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍)))) |
| 11 | 10 | biimpri 228 |
. 2
⊢ ((𝜑 ∧ ∃𝑓∃𝑔(𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → ∃𝑓∃𝑔(𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍)))) |
| 12 | | catcocl.b |
. . . 4
⊢ 𝐵 = (Base‘𝐶) |
| 13 | | catcocl.h |
. . . 4
⊢ 𝐻 = (Hom ‘𝐶) |
| 14 | | catcocl.o |
. . . 4
⊢ · =
(comp‘𝐶) |
| 15 | | catcocl.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 16 | 15 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → 𝐶 ∈ Cat) |
| 17 | | catcocl.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 18 | 17 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → 𝑋 ∈ 𝐵) |
| 19 | | catcocl.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 20 | 19 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → 𝑌 ∈ 𝐵) |
| 21 | | catcocl.z |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
| 22 | 21 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → 𝑍 ∈ 𝐵) |
| 23 | | simprl 771 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → 𝑓 ∈ (𝑋𝐻𝑌)) |
| 24 | | simprr 773 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → 𝑔 ∈ (𝑌𝐻𝑍)) |
| 25 | 12, 13, 14, 16, 18, 20, 22, 23, 24 | catcocl 17728 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → (𝑔(〈𝑋, 𝑌〉 · 𝑍)𝑓) ∈ (𝑋𝐻𝑍)) |
| 26 | 25 | 2eximi 1836 |
. 2
⊢
(∃𝑓∃𝑔(𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → ∃𝑓∃𝑔(𝑔(〈𝑋, 𝑌〉 · 𝑍)𝑓) ∈ (𝑋𝐻𝑍)) |
| 27 | | ne0i 4341 |
. . 3
⊢ ((𝑔(〈𝑋, 𝑌〉 · 𝑍)𝑓) ∈ (𝑋𝐻𝑍) → (𝑋𝐻𝑍) ≠ ∅) |
| 28 | 27 | exlimivv 1932 |
. 2
⊢
(∃𝑓∃𝑔(𝑔(〈𝑋, 𝑌〉 · 𝑍)𝑓) ∈ (𝑋𝐻𝑍) → (𝑋𝐻𝑍) ≠ ∅) |
| 29 | 9, 11, 26, 28 | 4syl 19 |
1
⊢ (𝜑 → (𝑋𝐻𝑍) ≠ ∅) |