Theorem isinv 17823

Description: Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.)

Hypotheses

Ref	Expression
invfval.b	⊢ 𝐵 = (Base‘𝐶)
invfval.n	⊢ 𝑁 = (Inv‘𝐶)
invfval.c	⊢ (𝜑 → 𝐶 ∈ Cat)
invfval.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
invfval.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
invfval.s	⊢ 𝑆 = (Sect‘𝐶)

Assertion

Ref	Expression
isinv	⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹)))

Proof of Theorem 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 17822	. . . 4 ⊢ (𝜑 → (𝑋𝑁𝑌) = ((𝑋𝑆𝑌) ∩ ◡(𝑌𝑆𝑋)))
8	7	breqd 5177	. . 3 ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ 𝐹((𝑋𝑆𝑌) ∩ ◡(𝑌𝑆𝑋))𝐺))
9		brin 5218	. . 3 ⊢ (𝐹((𝑋𝑆𝑌) ∩ ◡(𝑌𝑆𝑋))𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐹◡(𝑌𝑆𝑋)𝐺))
10	8, 9	bitrdi 287	. 2 ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐹◡(𝑌𝑆𝑋)𝐺)))
11		eqid 2740	. . . . . 6 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
12		eqid 2740	. . . . . 6 ⊢ (comp‘𝐶) = (comp‘𝐶)
13		eqid 2740	. . . . . 6 ⊢ (Id‘𝐶) = (Id‘𝐶)
14	1, 11, 12, 13, 6, 3, 5, 4	sectss 17815	. . . . 5 ⊢ (𝜑 → (𝑌𝑆𝑋) ⊆ ((𝑌(Hom ‘𝐶)𝑋) × (𝑋(Hom ‘𝐶)𝑌)))
15		relxp 5718	. . . . 5 ⊢ Rel ((𝑌(Hom ‘𝐶)𝑋) × (𝑋(Hom ‘𝐶)𝑌))
16		relss 5805	. . . . 5 ⊢ ((𝑌𝑆𝑋) ⊆ ((𝑌(Hom ‘𝐶)𝑋) × (𝑋(Hom ‘𝐶)𝑌)) → (Rel ((𝑌(Hom ‘𝐶)𝑋) × (𝑋(Hom ‘𝐶)𝑌)) → Rel (𝑌𝑆𝑋)))
17	14, 15, 16	mpisyl 21	. . . 4 ⊢ (𝜑 → Rel (𝑌𝑆𝑋))
18		relbrcnvg 6137	. . . 4 ⊢ (Rel (𝑌𝑆𝑋) → (𝐹◡(𝑌𝑆𝑋)𝐺 ↔ 𝐺(𝑌𝑆𝑋)𝐹))
19	17, 18	syl 17	. . 3 ⊢ (𝜑 → (𝐹◡(𝑌𝑆𝑋)𝐺 ↔ 𝐺(𝑌𝑆𝑋)𝐹))
20	19	anbi2d 629	. 2 ⊢ (𝜑 → ((𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐹◡(𝑌𝑆𝑋)𝐺) ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹)))
21	10, 20	bitrd 279	1 ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108   ∩ cin 3975   ⊆ wss 3976   class class class wbr 5166   × cxp 5698  ^◡ccnv 5699  Rel wrel 5705  ‘cfv 6575  (class class class)co 7450  Basecbs 17260  Hom chom 17324  compcco 17325  Catccat 17724  Idccid 17725  Sectcsect 17807  Invcinv 17808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7772

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6527  df-fun 6577  df-fn 6578  df-f 6579  df-f1 6580  df-fo 6581  df-f1o 6582  df-fv 6583  df-ov 7453  df-oprab 7454  df-mpo 7455  df-1st 8032  df-2nd 8033  df-sect 17810  df-inv 17811

This theorem is referenced by:  invsym  17825  invfun  17827  invco  17834  inveq  17837  monsect  17846  invid  17850  invcoisoid  17855  isocoinvid  17856  funcinv  17939  fthinv  17995  fucinv  18045  invfuc  18046  2initoinv  18079  2termoinv  18086  setcinv  18159  catcisolem  18179  catciso  18180  rngcinv  20661  ringcinv  20695  rngcinvALTV  48001  ringcinvALTV  48035  thincinv  48732