![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isinv | Structured version Visualization version GIF version |
Description: Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
Ref | Expression |
---|---|
invfval.b | ⊢ 𝐵 = (Base‘𝐶) |
invfval.n | ⊢ 𝑁 = (Inv‘𝐶) |
invfval.c | ⊢ (𝜑 → 𝐶 ∈ Cat) |
invfval.x | ⊢ (𝜑 → 𝑋 ∈ 𝐵) |
invfval.y | ⊢ (𝜑 → 𝑌 ∈ 𝐵) |
invfval.s | ⊢ 𝑆 = (Sect‘𝐶) |
Ref | Expression |
---|---|
isinv | ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | invfval.b | . . . . 5 ⊢ 𝐵 = (Base‘𝐶) | |
2 | invfval.n | . . . . 5 ⊢ 𝑁 = (Inv‘𝐶) | |
3 | invfval.c | . . . . 5 ⊢ (𝜑 → 𝐶 ∈ Cat) | |
4 | invfval.x | . . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵) | |
5 | invfval.y | . . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝐵) | |
6 | invfval.s | . . . . 5 ⊢ 𝑆 = (Sect‘𝐶) | |
7 | 1, 2, 3, 4, 5, 6 | invfval 16732 | . . . 4 ⊢ (𝜑 → (𝑋𝑁𝑌) = ((𝑋𝑆𝑌) ∩ ◡(𝑌𝑆𝑋))) |
8 | 7 | breqd 4855 | . . 3 ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ 𝐹((𝑋𝑆𝑌) ∩ ◡(𝑌𝑆𝑋))𝐺)) |
9 | brin 4896 | . . 3 ⊢ (𝐹((𝑋𝑆𝑌) ∩ ◡(𝑌𝑆𝑋))𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐹◡(𝑌𝑆𝑋)𝐺)) | |
10 | 8, 9 | syl6bb 279 | . 2 ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐹◡(𝑌𝑆𝑋)𝐺))) |
11 | eqid 2800 | . . . . . 6 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶) | |
12 | eqid 2800 | . . . . . 6 ⊢ (comp‘𝐶) = (comp‘𝐶) | |
13 | eqid 2800 | . . . . . 6 ⊢ (Id‘𝐶) = (Id‘𝐶) | |
14 | 1, 11, 12, 13, 6, 3, 5, 4 | sectss 16725 | . . . . 5 ⊢ (𝜑 → (𝑌𝑆𝑋) ⊆ ((𝑌(Hom ‘𝐶)𝑋) × (𝑋(Hom ‘𝐶)𝑌))) |
15 | relxp 5331 | . . . . 5 ⊢ Rel ((𝑌(Hom ‘𝐶)𝑋) × (𝑋(Hom ‘𝐶)𝑌)) | |
16 | relss 5412 | . . . . 5 ⊢ ((𝑌𝑆𝑋) ⊆ ((𝑌(Hom ‘𝐶)𝑋) × (𝑋(Hom ‘𝐶)𝑌)) → (Rel ((𝑌(Hom ‘𝐶)𝑋) × (𝑋(Hom ‘𝐶)𝑌)) → Rel (𝑌𝑆𝑋))) | |
17 | 14, 15, 16 | mpisyl 21 | . . . 4 ⊢ (𝜑 → Rel (𝑌𝑆𝑋)) |
18 | relbrcnvg 5722 | . . . 4 ⊢ (Rel (𝑌𝑆𝑋) → (𝐹◡(𝑌𝑆𝑋)𝐺 ↔ 𝐺(𝑌𝑆𝑋)𝐹)) | |
19 | 17, 18 | syl 17 | . . 3 ⊢ (𝜑 → (𝐹◡(𝑌𝑆𝑋)𝐺 ↔ 𝐺(𝑌𝑆𝑋)𝐹)) |
20 | 19 | anbi2d 623 | . 2 ⊢ (𝜑 → ((𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐹◡(𝑌𝑆𝑋)𝐺) ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹))) |
21 | 10, 20 | bitrd 271 | 1 ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 385 = wceq 1653 ∈ wcel 2157 ∩ cin 3769 ⊆ wss 3770 class class class wbr 4844 × cxp 5311 ◡ccnv 5312 Rel wrel 5318 ‘cfv 6102 (class class class)co 6879 Basecbs 16183 Hom chom 16277 compcco 16278 Catccat 16638 Idccid 16639 Sectcsect 16717 Invcinv 16718 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2378 ax-ext 2778 ax-rep 4965 ax-sep 4976 ax-nul 4984 ax-pow 5036 ax-pr 5098 ax-un 7184 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2592 df-eu 2610 df-clab 2787 df-cleq 2793 df-clel 2796 df-nfc 2931 df-ne 2973 df-ral 3095 df-rex 3096 df-reu 3097 df-rab 3099 df-v 3388 df-sbc 3635 df-csb 3730 df-dif 3773 df-un 3775 df-in 3777 df-ss 3784 df-nul 4117 df-if 4279 df-pw 4352 df-sn 4370 df-pr 4372 df-op 4376 df-uni 4630 df-iun 4713 df-br 4845 df-opab 4907 df-mpt 4924 df-id 5221 df-xp 5319 df-rel 5320 df-cnv 5321 df-co 5322 df-dm 5323 df-rn 5324 df-res 5325 df-ima 5326 df-iota 6065 df-fun 6104 df-fn 6105 df-f 6106 df-f1 6107 df-fo 6108 df-f1o 6109 df-fv 6110 df-ov 6882 df-oprab 6883 df-mpt2 6884 df-1st 7402 df-2nd 7403 df-sect 16720 df-inv 16721 |
This theorem is referenced by: invsym 16735 invfun 16737 invco 16744 inveq 16747 monsect 16756 invid 16760 invcoisoid 16765 isocoinvid 16766 cicref 16774 funcinv 16846 fthinv 16899 fucinv 16946 invfuc 16947 2initoinv 16973 2termoinv 16980 setcinv 17053 catcisolem 17069 catciso 17070 rngcinv 42775 rngcinvALTV 42787 ringcinv 42826 ringcinvALTV 42850 |
Copyright terms: Public domain | W3C validator |