| Step | Hyp | Ref
| Expression |
| 1 | | fthmon.b |
. . 3
⊢ 𝐵 = (Base‘𝐶) |
| 2 | | ffthiso.s |
. . 3
⊢ 𝐼 = (Iso‘𝐶) |
| 3 | | ffthiso.t |
. . 3
⊢ 𝐽 = (Iso‘𝐷) |
| 4 | | fthmon.f |
. . . . 5
⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) |
| 5 | | fthfunc 17954 |
. . . . . 6
⊢ (𝐶 Faith 𝐷) ⊆ (𝐶 Func 𝐷) |
| 6 | 5 | ssbri 5188 |
. . . . 5
⊢ (𝐹(𝐶 Faith 𝐷)𝐺 → 𝐹(𝐶 Func 𝐷)𝐺) |
| 7 | 4, 6 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) |
| 8 | 7 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ∈ (𝑋𝐼𝑌)) → 𝐹(𝐶 Func 𝐷)𝐺) |
| 9 | | fthmon.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 10 | 9 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ∈ (𝑋𝐼𝑌)) → 𝑋 ∈ 𝐵) |
| 11 | | fthmon.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 12 | 11 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ∈ (𝑋𝐼𝑌)) → 𝑌 ∈ 𝐵) |
| 13 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ∈ (𝑋𝐼𝑌)) → 𝑅 ∈ (𝑋𝐼𝑌)) |
| 14 | 1, 2, 3, 8, 10, 12, 13 | funciso 17919 |
. 2
⊢ ((𝜑 ∧ 𝑅 ∈ (𝑋𝐼𝑌)) → ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) |
| 15 | | eqid 2737 |
. . . 4
⊢
(Inv‘𝐶) =
(Inv‘𝐶) |
| 16 | | df-br 5144 |
. . . . . . . 8
⊢ (𝐹(𝐶 Func 𝐷)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) |
| 17 | 7, 16 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) |
| 18 | | funcrcl 17908 |
. . . . . . 7
⊢
(〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
| 19 | 17, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
| 20 | 19 | simpld 494 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 21 | 20 | ad3antrrr 730 |
. . . 4
⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝐶 ∈ Cat) |
| 22 | 9 | ad3antrrr 730 |
. . . 4
⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑋 ∈ 𝐵) |
| 23 | 11 | ad3antrrr 730 |
. . . 4
⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑌 ∈ 𝐵) |
| 24 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 25 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Inv‘𝐷) =
(Inv‘𝐷) |
| 26 | 19 | simprd 495 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ Cat) |
| 27 | 1, 24, 7 | funcf1 17911 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝐵⟶(Base‘𝐷)) |
| 28 | 27, 9 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝑋) ∈ (Base‘𝐷)) |
| 29 | 27, 11 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝑌) ∈ (Base‘𝐷)) |
| 30 | 24, 25, 26, 28, 29, 3 | isoval 17809 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐹‘𝑋)𝐽(𝐹‘𝑌)) = dom ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))) |
| 31 | 30 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ↔ ((𝑋𝐺𝑌)‘𝑅) ∈ dom ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌)))) |
| 32 | 31 | biimpa 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → ((𝑋𝐺𝑌)‘𝑅) ∈ dom ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))) |
| 33 | 24, 25, 26, 28, 29 | invfun 17808 |
. . . . . . . . . 10
⊢ (𝜑 → Fun ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))) |
| 34 | 33 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → Fun ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))) |
| 35 | | funfvbrb 7071 |
. . . . . . . . 9
⊢ (Fun
((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌)) → (((𝑋𝐺𝑌)‘𝑅) ∈ dom ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌)) ↔ ((𝑋𝐺𝑌)‘𝑅)((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))(((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)))) |
| 36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → (((𝑋𝐺𝑌)‘𝑅) ∈ dom ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌)) ↔ ((𝑋𝐺𝑌)‘𝑅)((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))(((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)))) |
| 37 | 32, 36 | mpbid 232 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → ((𝑋𝐺𝑌)‘𝑅)((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))(((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅))) |
| 38 | 37 | ad2antrr 726 |
. . . . . 6
⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → ((𝑋𝐺𝑌)‘𝑅)((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))(((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅))) |
| 39 | | simpr 484 |
. . . . . 6
⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) |
| 40 | 38, 39 | breqtrd 5169 |
. . . . 5
⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → ((𝑋𝐺𝑌)‘𝑅)((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑓)) |
| 41 | | fthmon.h |
. . . . . 6
⊢ 𝐻 = (Hom ‘𝐶) |
| 42 | 4 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝐹(𝐶 Faith 𝐷)𝐺) |
| 43 | | fthmon.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) |
| 44 | 43 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑅 ∈ (𝑋𝐻𝑌)) |
| 45 | | simplr 769 |
. . . . . 6
⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑓 ∈ (𝑌𝐻𝑋)) |
| 46 | 1, 41, 42, 22, 23, 44, 45, 15, 25 | fthinv 17973 |
. . . . 5
⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → (𝑅(𝑋(Inv‘𝐶)𝑌)𝑓 ↔ ((𝑋𝐺𝑌)‘𝑅)((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑓))) |
| 47 | 40, 46 | mpbird 257 |
. . . 4
⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑅(𝑋(Inv‘𝐶)𝑌)𝑓) |
| 48 | 1, 15, 21, 22, 23, 2, 47 | inviso1 17810 |
. . 3
⊢ ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑅 ∈ (𝑋𝐼𝑌)) |
| 49 | | eqid 2737 |
. . . 4
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
| 50 | | ffthiso.f |
. . . . 5
⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) |
| 51 | 50 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → 𝐹(𝐶 Full 𝐷)𝐺) |
| 52 | 11 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → 𝑌 ∈ 𝐵) |
| 53 | 9 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → 𝑋 ∈ 𝐵) |
| 54 | 24, 49, 3, 26, 29, 28 | isohom 17820 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝑌)𝐽(𝐹‘𝑋)) ⊆ ((𝐹‘𝑌)(Hom ‘𝐷)(𝐹‘𝑋))) |
| 55 | 54 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → ((𝐹‘𝑌)𝐽(𝐹‘𝑋)) ⊆ ((𝐹‘𝑌)(Hom ‘𝐷)(𝐹‘𝑋))) |
| 56 | 24, 25, 26, 28, 29, 3 | invf 17812 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌)):((𝐹‘𝑋)𝐽(𝐹‘𝑌))⟶((𝐹‘𝑌)𝐽(𝐹‘𝑋))) |
| 57 | 56 | ffvelcdmda 7104 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) ∈ ((𝐹‘𝑌)𝐽(𝐹‘𝑋))) |
| 58 | 55, 57 | sseldd 3984 |
. . . 4
⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → (((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) ∈ ((𝐹‘𝑌)(Hom ‘𝐷)(𝐹‘𝑋))) |
| 59 | 1, 49, 41, 51, 52, 53, 58 | fulli 17960 |
. . 3
⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → ∃𝑓 ∈ (𝑌𝐻𝑋)(((𝐹‘𝑋)(Inv‘𝐷)(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) |
| 60 | 48, 59 | r19.29a 3162 |
. 2
⊢ ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌))) → 𝑅 ∈ (𝑋𝐼𝑌)) |
| 61 | 14, 60 | impbida 801 |
1
⊢ (𝜑 → (𝑅 ∈ (𝑋𝐼𝑌) ↔ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))) |