Proof of Theorem isepi2
Step | Hyp | Ref
| Expression |
1 | | isepi.b |
. . 3
⊢ 𝐵 = (Base‘𝐶) |
2 | | isepi.h |
. . 3
⊢ 𝐻 = (Hom ‘𝐶) |
3 | | isepi.o |
. . 3
⊢ · =
(comp‘𝐶) |
4 | | isepi.e |
. . 3
⊢ 𝐸 = (Epi‘𝐶) |
5 | | isepi.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
6 | | isepi.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
7 | | isepi.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
8 | 1, 2, 3, 4, 5, 6, 7 | isepi 17433 |
. 2
⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹))))) |
9 | 5 | ad2antrr 722 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐻𝑌)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑔 ∈ (𝑌𝐻𝑧))) → 𝐶 ∈ Cat) |
10 | 6 | ad2antrr 722 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐻𝑌)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑔 ∈ (𝑌𝐻𝑧))) → 𝑋 ∈ 𝐵) |
11 | 7 | ad2antrr 722 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐻𝑌)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑔 ∈ (𝑌𝐻𝑧))) → 𝑌 ∈ 𝐵) |
12 | | simprl 767 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐻𝑌)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑔 ∈ (𝑌𝐻𝑧))) → 𝑧 ∈ 𝐵) |
13 | | simplr 765 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐻𝑌)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑔 ∈ (𝑌𝐻𝑧))) → 𝐹 ∈ (𝑋𝐻𝑌)) |
14 | | simprr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐻𝑌)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑔 ∈ (𝑌𝐻𝑧))) → 𝑔 ∈ (𝑌𝐻𝑧)) |
15 | 1, 2, 3, 9, 10, 11, 12, 13, 14 | catcocl 17375 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐻𝑌)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑔 ∈ (𝑌𝐻𝑧))) → (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) ∈ (𝑋𝐻𝑧)) |
16 | 15 | anassrs 467 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐹 ∈ (𝑋𝐻𝑌)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑌𝐻𝑧)) → (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) ∈ (𝑋𝐻𝑧)) |
17 | 16 | ralrimiva 3109 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐻𝑌)) ∧ 𝑧 ∈ 𝐵) → ∀𝑔 ∈ (𝑌𝐻𝑧)(𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) ∈ (𝑋𝐻𝑧)) |
18 | | eqid 2739 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)) = (𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)) |
19 | 18 | fmpt 6978 |
. . . . . . 7
⊢
(∀𝑔 ∈
(𝑌𝐻𝑧)(𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) ∈ (𝑋𝐻𝑧) ↔ (𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)):(𝑌𝐻𝑧)⟶(𝑋𝐻𝑧)) |
20 | | df-f1 6435 |
. . . . . . . 8
⊢ ((𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)):(𝑌𝐻𝑧)–1-1→(𝑋𝐻𝑧) ↔ ((𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)):(𝑌𝐻𝑧)⟶(𝑋𝐻𝑧) ∧ Fun ◡(𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)))) |
21 | 20 | baib 535 |
. . . . . . 7
⊢ ((𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)):(𝑌𝐻𝑧)⟶(𝑋𝐻𝑧) → ((𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)):(𝑌𝐻𝑧)–1-1→(𝑋𝐻𝑧) ↔ Fun ◡(𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)))) |
22 | 19, 21 | sylbi 216 |
. . . . . 6
⊢
(∀𝑔 ∈
(𝑌𝐻𝑧)(𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) ∈ (𝑋𝐻𝑧) → ((𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)):(𝑌𝐻𝑧)–1-1→(𝑋𝐻𝑧) ↔ Fun ◡(𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)))) |
23 | | oveq1 7275 |
. . . . . . . 8
⊢ (𝑔 = ℎ → (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉 · 𝑧)𝐹)) |
24 | 18, 23 | f1mpt 7128 |
. . . . . . 7
⊢ ((𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)):(𝑌𝐻𝑧)–1-1→(𝑋𝐻𝑧) ↔ (∀𝑔 ∈ (𝑌𝐻𝑧)(𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) ∈ (𝑋𝐻𝑧) ∧ ∀𝑔 ∈ (𝑌𝐻𝑧)∀ℎ ∈ (𝑌𝐻𝑧)((𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉 · 𝑧)𝐹) → 𝑔 = ℎ))) |
25 | 24 | baib 535 |
. . . . . 6
⊢
(∀𝑔 ∈
(𝑌𝐻𝑧)(𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) ∈ (𝑋𝐻𝑧) → ((𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)):(𝑌𝐻𝑧)–1-1→(𝑋𝐻𝑧) ↔ ∀𝑔 ∈ (𝑌𝐻𝑧)∀ℎ ∈ (𝑌𝐻𝑧)((𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉 · 𝑧)𝐹) → 𝑔 = ℎ))) |
26 | 22, 25 | bitr3d 280 |
. . . . 5
⊢
(∀𝑔 ∈
(𝑌𝐻𝑧)(𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) ∈ (𝑋𝐻𝑧) → (Fun ◡(𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)) ↔ ∀𝑔 ∈ (𝑌𝐻𝑧)∀ℎ ∈ (𝑌𝐻𝑧)((𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉 · 𝑧)𝐹) → 𝑔 = ℎ))) |
27 | 17, 26 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐻𝑌)) ∧ 𝑧 ∈ 𝐵) → (Fun ◡(𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)) ↔ ∀𝑔 ∈ (𝑌𝐻𝑧)∀ℎ ∈ (𝑌𝐻𝑧)((𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉 · 𝑧)𝐹) → 𝑔 = ℎ))) |
28 | 27 | ralbidva 3121 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐻𝑌)) → (∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹)) ↔ ∀𝑧 ∈ 𝐵 ∀𝑔 ∈ (𝑌𝐻𝑧)∀ℎ ∈ (𝑌𝐻𝑧)((𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉 · 𝑧)𝐹) → 𝑔 = ℎ))) |
29 | 28 | pm5.32da 578 |
. 2
⊢ (𝜑 → ((𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹))) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 ∀𝑔 ∈ (𝑌𝐻𝑧)∀ℎ ∈ (𝑌𝐻𝑧)((𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉 · 𝑧)𝐹) → 𝑔 = ℎ)))) |
30 | 8, 29 | bitrd 278 |
1
⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 ∀𝑔 ∈ (𝑌𝐻𝑧)∀ℎ ∈ (𝑌𝐻𝑧)((𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉 · 𝑧)𝐹) → 𝑔 = ℎ)))) |