| Step | Hyp | Ref
| Expression |
| 1 | | relfull 17955 |
. 2
⊢ Rel
(𝐴 Full 𝐶) |
| 2 | | relfull 17955 |
. 2
⊢ Rel
(𝐵 Full 𝐷) |
| 3 | | fullpropd.1 |
. . . . . . . 8
⊢ (𝜑 → (Homf
‘𝐴) =
(Homf ‘𝐵)) |
| 4 | 3 | homfeqbas 17739 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝐴) = (Base‘𝐵)) |
| 5 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓(𝐴 Func 𝐶)𝑔) → (Base‘𝐴) = (Base‘𝐵)) |
| 6 | 5 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓(𝐴 Func 𝐶)𝑔) ∧ 𝑥 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵)) |
| 7 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 8 | | eqid 2737 |
. . . . . . . . 9
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 9 | | eqid 2737 |
. . . . . . . . 9
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
| 10 | | fullpropd.3 |
. . . . . . . . . 10
⊢ (𝜑 → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
| 11 | 10 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓(𝐴 Func 𝐶)𝑔) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
| 12 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝐴) =
(Base‘𝐴) |
| 13 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓(𝐴 Func 𝐶)𝑔) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) → 𝑓(𝐴 Func 𝐶)𝑔) |
| 14 | 12, 7, 13 | funcf1 17911 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓(𝐴 Func 𝐶)𝑔) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) |
| 15 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓(𝐴 Func 𝐶)𝑔) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) → 𝑥 ∈ (Base‘𝐴)) |
| 16 | 14, 15 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓(𝐴 Func 𝐶)𝑔) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) → (𝑓‘𝑥) ∈ (Base‘𝐶)) |
| 17 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓(𝐴 Func 𝐶)𝑔) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) → 𝑦 ∈ (Base‘𝐴)) |
| 18 | 14, 17 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓(𝐴 Func 𝐶)𝑔) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) → (𝑓‘𝑦) ∈ (Base‘𝐶)) |
| 19 | 7, 8, 9, 11, 16, 18 | homfeqval 17740 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓(𝐴 Func 𝐶)𝑔) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) → ((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) = ((𝑓‘𝑥)(Hom ‘𝐷)(𝑓‘𝑦))) |
| 20 | 19 | eqeq2d 2748 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓(𝐴 Func 𝐶)𝑔) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) → (ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↔ ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝐷)(𝑓‘𝑦)))) |
| 21 | 6, 20 | raleqbidva 3332 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓(𝐴 Func 𝐶)𝑔) ∧ 𝑥 ∈ (Base‘𝐴)) → (∀𝑦 ∈ (Base‘𝐴)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↔ ∀𝑦 ∈ (Base‘𝐵)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝐷)(𝑓‘𝑦)))) |
| 22 | 5, 21 | raleqbidva 3332 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓(𝐴 Func 𝐶)𝑔) → (∀𝑥 ∈ (Base‘𝐴)∀𝑦 ∈ (Base‘𝐴)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↔ ∀𝑥 ∈ (Base‘𝐵)∀𝑦 ∈ (Base‘𝐵)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝐷)(𝑓‘𝑦)))) |
| 23 | 22 | pm5.32da 579 |
. . . 4
⊢ (𝜑 → ((𝑓(𝐴 Func 𝐶)𝑔 ∧ ∀𝑥 ∈ (Base‘𝐴)∀𝑦 ∈ (Base‘𝐴)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦))) ↔ (𝑓(𝐴 Func 𝐶)𝑔 ∧ ∀𝑥 ∈ (Base‘𝐵)∀𝑦 ∈ (Base‘𝐵)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝐷)(𝑓‘𝑦))))) |
| 24 | | fullpropd.2 |
. . . . . . 7
⊢ (𝜑 →
(compf‘𝐴) = (compf‘𝐵)) |
| 25 | | fullpropd.4 |
. . . . . . 7
⊢ (𝜑 →
(compf‘𝐶) = (compf‘𝐷)) |
| 26 | | fullpropd.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 27 | | fullpropd.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
| 28 | | fullpropd.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
| 29 | | fullpropd.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
| 30 | 3, 24, 10, 25, 26, 27, 28, 29 | funcpropd 17947 |
. . . . . 6
⊢ (𝜑 → (𝐴 Func 𝐶) = (𝐵 Func 𝐷)) |
| 31 | 30 | breqd 5154 |
. . . . 5
⊢ (𝜑 → (𝑓(𝐴 Func 𝐶)𝑔 ↔ 𝑓(𝐵 Func 𝐷)𝑔)) |
| 32 | 31 | anbi1d 631 |
. . . 4
⊢ (𝜑 → ((𝑓(𝐴 Func 𝐶)𝑔 ∧ ∀𝑥 ∈ (Base‘𝐵)∀𝑦 ∈ (Base‘𝐵)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝐷)(𝑓‘𝑦))) ↔ (𝑓(𝐵 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ (Base‘𝐵)∀𝑦 ∈ (Base‘𝐵)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝐷)(𝑓‘𝑦))))) |
| 33 | 23, 32 | bitrd 279 |
. . 3
⊢ (𝜑 → ((𝑓(𝐴 Func 𝐶)𝑔 ∧ ∀𝑥 ∈ (Base‘𝐴)∀𝑦 ∈ (Base‘𝐴)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦))) ↔ (𝑓(𝐵 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ (Base‘𝐵)∀𝑦 ∈ (Base‘𝐵)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝐷)(𝑓‘𝑦))))) |
| 34 | 12, 8 | isfull 17957 |
. . 3
⊢ (𝑓(𝐴 Full 𝐶)𝑔 ↔ (𝑓(𝐴 Func 𝐶)𝑔 ∧ ∀𝑥 ∈ (Base‘𝐴)∀𝑦 ∈ (Base‘𝐴)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)))) |
| 35 | | eqid 2737 |
. . . 4
⊢
(Base‘𝐵) =
(Base‘𝐵) |
| 36 | 35, 9 | isfull 17957 |
. . 3
⊢ (𝑓(𝐵 Full 𝐷)𝑔 ↔ (𝑓(𝐵 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ (Base‘𝐵)∀𝑦 ∈ (Base‘𝐵)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝐷)(𝑓‘𝑦)))) |
| 37 | 33, 34, 36 | 3bitr4g 314 |
. 2
⊢ (𝜑 → (𝑓(𝐴 Full 𝐶)𝑔 ↔ 𝑓(𝐵 Full 𝐷)𝑔)) |
| 38 | 1, 2, 37 | eqbrrdiv 5804 |
1
⊢ (𝜑 → (𝐴 Full 𝐶) = (𝐵 Full 𝐷)) |