MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  invfuc Structured version   Visualization version   GIF version

Theorem invfuc 17991
Description: If 𝑉(𝑥) is an inverse to 𝑈(𝑥) for each 𝑥, and 𝑈 is a natural transformation, then 𝑉 is also a natural transformation, and they are inverse in the functor category. (Contributed by Mario Carneiro, 28-Jan-2017.)
Hypotheses
Ref Expression
fuciso.q 𝑄 = (𝐶 FuncCat 𝐷)
fuciso.b 𝐵 = (Base‘𝐶)
fuciso.n 𝑁 = (𝐶 Nat 𝐷)
fuciso.f (𝜑𝐹 ∈ (𝐶 Func 𝐷))
fuciso.g (𝜑𝐺 ∈ (𝐶 Func 𝐷))
fucinv.i 𝐼 = (Inv‘𝑄)
fucinv.j 𝐽 = (Inv‘𝐷)
invfuc.u (𝜑𝑈 ∈ (𝐹𝑁𝐺))
invfuc.v ((𝜑𝑥𝐵) → (𝑈𝑥)(((1st𝐹)‘𝑥)𝐽((1st𝐺)‘𝑥))𝑋)
Assertion
Ref Expression
invfuc (𝜑𝑈(𝐹𝐼𝐺)(𝑥𝐵𝑋))
Distinct variable groups:   𝑥,𝐵   𝑥,𝐶   𝑥,𝐷   𝑥,𝐼   𝑥,𝐹   𝑥,𝐺   𝑥,𝐽   𝑥,𝑁   𝜑,𝑥   𝑥,𝑄   𝑥,𝑈
Allowed substitution hint:   𝑋(𝑥)

Proof of Theorem invfuc
Dummy variables 𝑦 𝑓 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 invfuc.u . 2 (𝜑𝑈 ∈ (𝐹𝑁𝐺))
2 invfuc.v . . . . . . . 8 ((𝜑𝑥𝐵) → (𝑈𝑥)(((1st𝐹)‘𝑥)𝐽((1st𝐺)‘𝑥))𝑋)
3 eqid 2726 . . . . . . . . . 10 (Base‘𝐷) = (Base‘𝐷)
4 fucinv.j . . . . . . . . . 10 𝐽 = (Inv‘𝐷)
5 fuciso.f . . . . . . . . . . . . 13 (𝜑𝐹 ∈ (𝐶 Func 𝐷))
6 funcrcl 17874 . . . . . . . . . . . . 13 (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
75, 6syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
87simprd 494 . . . . . . . . . . 11 (𝜑𝐷 ∈ Cat)
98adantr 479 . . . . . . . . . 10 ((𝜑𝑥𝐵) → 𝐷 ∈ Cat)
10 fuciso.b . . . . . . . . . . . 12 𝐵 = (Base‘𝐶)
11 relfunc 17873 . . . . . . . . . . . . 13 Rel (𝐶 Func 𝐷)
12 1st2ndbr 8045 . . . . . . . . . . . . 13 ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
1311, 5, 12sylancr 585 . . . . . . . . . . . 12 (𝜑 → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
1410, 3, 13funcf1 17877 . . . . . . . . . . 11 (𝜑 → (1st𝐹):𝐵⟶(Base‘𝐷))
1514ffvelcdmda 7087 . . . . . . . . . 10 ((𝜑𝑥𝐵) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
16 fuciso.g . . . . . . . . . . . . 13 (𝜑𝐺 ∈ (𝐶 Func 𝐷))
17 1st2ndbr 8045 . . . . . . . . . . . . 13 ((Rel (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → (1st𝐺)(𝐶 Func 𝐷)(2nd𝐺))
1811, 16, 17sylancr 585 . . . . . . . . . . . 12 (𝜑 → (1st𝐺)(𝐶 Func 𝐷)(2nd𝐺))
1910, 3, 18funcf1 17877 . . . . . . . . . . 11 (𝜑 → (1st𝐺):𝐵⟶(Base‘𝐷))
2019ffvelcdmda 7087 . . . . . . . . . 10 ((𝜑𝑥𝐵) → ((1st𝐺)‘𝑥) ∈ (Base‘𝐷))
21 eqid 2726 . . . . . . . . . 10 (Hom ‘𝐷) = (Hom ‘𝐷)
223, 4, 9, 15, 20, 21invss 17769 . . . . . . . . 9 ((𝜑𝑥𝐵) → (((1st𝐹)‘𝑥)𝐽((1st𝐺)‘𝑥)) ⊆ ((((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐺)‘𝑥)) × (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥))))
2322ssbrd 5186 . . . . . . . 8 ((𝜑𝑥𝐵) → ((𝑈𝑥)(((1st𝐹)‘𝑥)𝐽((1st𝐺)‘𝑥))𝑋 → (𝑈𝑥)((((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐺)‘𝑥)) × (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥)))𝑋))
242, 23mpd 15 . . . . . . 7 ((𝜑𝑥𝐵) → (𝑈𝑥)((((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐺)‘𝑥)) × (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥)))𝑋)
25 brxp 5721 . . . . . . . 8 ((𝑈𝑥)((((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐺)‘𝑥)) × (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥)))𝑋 ↔ ((𝑈𝑥) ∈ (((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐺)‘𝑥)) ∧ 𝑋 ∈ (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥))))
2625simprbi 495 . . . . . . 7 ((𝑈𝑥)((((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐺)‘𝑥)) × (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥)))𝑋𝑋 ∈ (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥)))
2724, 26syl 17 . . . . . 6 ((𝜑𝑥𝐵) → 𝑋 ∈ (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥)))
2827ralrimiva 3136 . . . . 5 (𝜑 → ∀𝑥𝐵 𝑋 ∈ (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥)))
2910fvexi 6904 . . . . . 6 𝐵 ∈ V
30 mptelixpg 8953 . . . . . 6 (𝐵 ∈ V → ((𝑥𝐵𝑋) ∈ X𝑥𝐵 (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥)) ↔ ∀𝑥𝐵 𝑋 ∈ (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥))))
3129, 30ax-mp 5 . . . . 5 ((𝑥𝐵𝑋) ∈ X𝑥𝐵 (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥)) ↔ ∀𝑥𝐵 𝑋 ∈ (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥)))
3228, 31sylibr 233 . . . 4 (𝜑 → (𝑥𝐵𝑋) ∈ X𝑥𝐵 (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥)))
33 fveq2 6890 . . . . . 6 (𝑥 = 𝑦 → ((1st𝐺)‘𝑥) = ((1st𝐺)‘𝑦))
34 fveq2 6890 . . . . . 6 (𝑥 = 𝑦 → ((1st𝐹)‘𝑥) = ((1st𝐹)‘𝑦))
3533, 34oveq12d 7431 . . . . 5 (𝑥 = 𝑦 → (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥)) = (((1st𝐺)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
3635cbvixpv 8933 . . . 4 X𝑥𝐵 (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥)) = X𝑦𝐵 (((1st𝐺)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑦))
3732, 36eleqtrdi 2836 . . 3 (𝜑 → (𝑥𝐵𝑋) ∈ X𝑦𝐵 (((1st𝐺)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
38 simpr2 1192 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑧𝐵)
39 simpr 483 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐵) → 𝑥𝐵)
40 eqid 2726 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐵𝑋) = (𝑥𝐵𝑋)
4140fvmpt2 7009 . . . . . . . . . . . . . . . . . 18 ((𝑥𝐵𝑋 ∈ (((1st𝐺)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑥))) → ((𝑥𝐵𝑋)‘𝑥) = 𝑋)
4239, 27, 41syl2anc 582 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐵) → ((𝑥𝐵𝑋)‘𝑥) = 𝑋)
432, 42breqtrrd 5171 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐵) → (𝑈𝑥)(((1st𝐹)‘𝑥)𝐽((1st𝐺)‘𝑥))((𝑥𝐵𝑋)‘𝑥))
4443ralrimiva 3136 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑥𝐵 (𝑈𝑥)(((1st𝐹)‘𝑥)𝐽((1st𝐺)‘𝑥))((𝑥𝐵𝑋)‘𝑥))
4544adantr 479 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ∀𝑥𝐵 (𝑈𝑥)(((1st𝐹)‘𝑥)𝐽((1st𝐺)‘𝑥))((𝑥𝐵𝑋)‘𝑥))
46 nfcv 2892 . . . . . . . . . . . . . . . 16 𝑥(𝑈𝑧)
47 nfcv 2892 . . . . . . . . . . . . . . . 16 𝑥(((1st𝐹)‘𝑧)𝐽((1st𝐺)‘𝑧))
48 nffvmpt1 6901 . . . . . . . . . . . . . . . 16 𝑥((𝑥𝐵𝑋)‘𝑧)
4946, 47, 48nfbr 5190 . . . . . . . . . . . . . . 15 𝑥(𝑈𝑧)(((1st𝐹)‘𝑧)𝐽((1st𝐺)‘𝑧))((𝑥𝐵𝑋)‘𝑧)
50 fveq2 6890 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (𝑈𝑥) = (𝑈𝑧))
51 fveq2 6890 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → ((1st𝐹)‘𝑥) = ((1st𝐹)‘𝑧))
52 fveq2 6890 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → ((1st𝐺)‘𝑥) = ((1st𝐺)‘𝑧))
5351, 52oveq12d 7431 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (((1st𝐹)‘𝑥)𝐽((1st𝐺)‘𝑥)) = (((1st𝐹)‘𝑧)𝐽((1st𝐺)‘𝑧)))
54 fveq2 6890 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → ((𝑥𝐵𝑋)‘𝑥) = ((𝑥𝐵𝑋)‘𝑧))
5550, 53, 54breq123d 5157 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → ((𝑈𝑥)(((1st𝐹)‘𝑥)𝐽((1st𝐺)‘𝑥))((𝑥𝐵𝑋)‘𝑥) ↔ (𝑈𝑧)(((1st𝐹)‘𝑧)𝐽((1st𝐺)‘𝑧))((𝑥𝐵𝑋)‘𝑧)))
5649, 55rspc 3595 . . . . . . . . . . . . . 14 (𝑧𝐵 → (∀𝑥𝐵 (𝑈𝑥)(((1st𝐹)‘𝑥)𝐽((1st𝐺)‘𝑥))((𝑥𝐵𝑋)‘𝑥) → (𝑈𝑧)(((1st𝐹)‘𝑧)𝐽((1st𝐺)‘𝑧))((𝑥𝐵𝑋)‘𝑧)))
5738, 45, 56sylc 65 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈𝑧)(((1st𝐹)‘𝑧)𝐽((1st𝐺)‘𝑧))((𝑥𝐵𝑋)‘𝑧))
588adantr 479 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐷 ∈ Cat)
5914adantr 479 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st𝐹):𝐵⟶(Base‘𝐷))
6059, 38ffvelcdmd 7088 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st𝐹)‘𝑧) ∈ (Base‘𝐷))
6119adantr 479 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st𝐺):𝐵⟶(Base‘𝐷))
6261, 38ffvelcdmd 7088 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st𝐺)‘𝑧) ∈ (Base‘𝐷))
63 eqid 2726 . . . . . . . . . . . . . 14 (Sect‘𝐷) = (Sect‘𝐷)
643, 4, 58, 60, 62, 63isinv 17768 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈𝑧)(((1st𝐹)‘𝑧)𝐽((1st𝐺)‘𝑧))((𝑥𝐵𝑋)‘𝑧) ↔ ((𝑈𝑧)(((1st𝐹)‘𝑧)(Sect‘𝐷)((1st𝐺)‘𝑧))((𝑥𝐵𝑋)‘𝑧) ∧ ((𝑥𝐵𝑋)‘𝑧)(((1st𝐺)‘𝑧)(Sect‘𝐷)((1st𝐹)‘𝑧))(𝑈𝑧))))
6557, 64mpbid 231 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈𝑧)(((1st𝐹)‘𝑧)(Sect‘𝐷)((1st𝐺)‘𝑧))((𝑥𝐵𝑋)‘𝑧) ∧ ((𝑥𝐵𝑋)‘𝑧)(((1st𝐺)‘𝑧)(Sect‘𝐷)((1st𝐹)‘𝑧))(𝑈𝑧)))
6665simpld 493 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈𝑧)(((1st𝐹)‘𝑧)(Sect‘𝐷)((1st𝐺)‘𝑧))((𝑥𝐵𝑋)‘𝑧))
67 eqid 2726 . . . . . . . . . . . 12 (comp‘𝐷) = (comp‘𝐷)
68 eqid 2726 . . . . . . . . . . . 12 (Id‘𝐷) = (Id‘𝐷)
693, 21, 67, 68, 63, 58, 60, 62issect 17761 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈𝑧)(((1st𝐹)‘𝑧)(Sect‘𝐷)((1st𝐺)‘𝑧))((𝑥𝐵𝑋)‘𝑧) ↔ ((𝑈𝑧) ∈ (((1st𝐹)‘𝑧)(Hom ‘𝐷)((1st𝐺)‘𝑧)) ∧ ((𝑥𝐵𝑋)‘𝑧) ∈ (((1st𝐺)‘𝑧)(Hom ‘𝐷)((1st𝐹)‘𝑧)) ∧ (((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐹)‘𝑧), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))(𝑈𝑧)) = ((Id‘𝐷)‘((1st𝐹)‘𝑧)))))
7066, 69mpbid 231 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈𝑧) ∈ (((1st𝐹)‘𝑧)(Hom ‘𝐷)((1st𝐺)‘𝑧)) ∧ ((𝑥𝐵𝑋)‘𝑧) ∈ (((1st𝐺)‘𝑧)(Hom ‘𝐷)((1st𝐹)‘𝑧)) ∧ (((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐹)‘𝑧), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))(𝑈𝑧)) = ((Id‘𝐷)‘((1st𝐹)‘𝑧))))
7170simp3d 1141 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐹)‘𝑧), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))(𝑈𝑧)) = ((Id‘𝐷)‘((1st𝐹)‘𝑧)))
7271oveq1d 7428 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐹)‘𝑧), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))(𝑈𝑧))(⟨((1st𝐹)‘𝑦), ((1st𝐹)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑦(2nd𝐹)𝑧)‘𝑓)) = (((Id‘𝐷)‘((1st𝐹)‘𝑧))(⟨((1st𝐹)‘𝑦), ((1st𝐹)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑦(2nd𝐹)𝑧)‘𝑓)))
73 simpr1 1191 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑦𝐵)
7459, 73ffvelcdmd 7088 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st𝐹)‘𝑦) ∈ (Base‘𝐷))
75 eqid 2726 . . . . . . . . . . 11 (Hom ‘𝐶) = (Hom ‘𝐶)
7613adantr 479 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
7710, 75, 21, 76, 73, 38funcf2 17879 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
78 simpr3 1193 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))
7977, 78ffvelcdmd 7088 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd𝐹)𝑧)‘𝑓) ∈ (((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
803, 21, 68, 58, 74, 67, 60, 79catlid 17688 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((Id‘𝐷)‘((1st𝐹)‘𝑧))(⟨((1st𝐹)‘𝑦), ((1st𝐹)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑦(2nd𝐹)𝑧)‘𝑓)) = ((𝑦(2nd𝐹)𝑧)‘𝑓))
8172, 80eqtr2d 2767 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd𝐹)𝑧)‘𝑓) = ((((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐹)‘𝑧), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))(𝑈𝑧))(⟨((1st𝐹)‘𝑦), ((1st𝐹)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑦(2nd𝐹)𝑧)‘𝑓)))
82 fuciso.n . . . . . . . . 9 𝑁 = (𝐶 Nat 𝐷)
831adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑈 ∈ (𝐹𝑁𝐺))
8482, 83nat1st2nd 17966 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑈 ∈ (⟨(1st𝐹), (2nd𝐹)⟩𝑁⟨(1st𝐺), (2nd𝐺)⟩))
8582, 84, 10, 21, 38natcl 17968 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈𝑧) ∈ (((1st𝐹)‘𝑧)(Hom ‘𝐷)((1st𝐺)‘𝑧)))
8670simp2d 1140 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥𝐵𝑋)‘𝑧) ∈ (((1st𝐺)‘𝑧)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
873, 21, 67, 58, 74, 60, 62, 79, 85, 60, 86catass 17691 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐹)‘𝑧), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))(𝑈𝑧))(⟨((1st𝐹)‘𝑦), ((1st𝐹)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑦(2nd𝐹)𝑧)‘𝑓)) = (((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑈𝑧)(⟨((1st𝐹)‘𝑦), ((1st𝐹)‘𝑧)⟩(comp‘𝐷)((1st𝐺)‘𝑧))((𝑦(2nd𝐹)𝑧)‘𝑓))))
8882, 84, 10, 75, 67, 73, 38, 78nati 17970 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈𝑧)(⟨((1st𝐹)‘𝑦), ((1st𝐹)‘𝑧)⟩(comp‘𝐷)((1st𝐺)‘𝑧))((𝑦(2nd𝐹)𝑧)‘𝑓)) = (((𝑦(2nd𝐺)𝑧)‘𝑓)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))(𝑈𝑦)))
8988oveq2d 7429 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑈𝑧)(⟨((1st𝐹)‘𝑦), ((1st𝐹)‘𝑧)⟩(comp‘𝐷)((1st𝐺)‘𝑧))((𝑦(2nd𝐹)𝑧)‘𝑓))) = (((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))(((𝑦(2nd𝐺)𝑧)‘𝑓)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))(𝑈𝑦))))
9081, 87, 893eqtrd 2770 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd𝐹)𝑧)‘𝑓) = (((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))(((𝑦(2nd𝐺)𝑧)‘𝑓)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))(𝑈𝑦))))
9190oveq1d 7428 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd𝐹)𝑧)‘𝑓)(⟨((1st𝐺)‘𝑦), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥𝐵𝑋)‘𝑦)) = ((((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))(((𝑦(2nd𝐺)𝑧)‘𝑓)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))(𝑈𝑦)))(⟨((1st𝐺)‘𝑦), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥𝐵𝑋)‘𝑦)))
9261, 73ffvelcdmd 7088 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st𝐺)‘𝑦) ∈ (Base‘𝐷))
93 nfcv 2892 . . . . . . . . . . . . 13 𝑥(𝑈𝑦)
94 nfcv 2892 . . . . . . . . . . . . 13 𝑥(((1st𝐹)‘𝑦)𝐽((1st𝐺)‘𝑦))
95 nffvmpt1 6901 . . . . . . . . . . . . 13 𝑥((𝑥𝐵𝑋)‘𝑦)
9693, 94, 95nfbr 5190 . . . . . . . . . . . 12 𝑥(𝑈𝑦)(((1st𝐹)‘𝑦)𝐽((1st𝐺)‘𝑦))((𝑥𝐵𝑋)‘𝑦)
97 fveq2 6890 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑈𝑥) = (𝑈𝑦))
9834, 33oveq12d 7431 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (((1st𝐹)‘𝑥)𝐽((1st𝐺)‘𝑥)) = (((1st𝐹)‘𝑦)𝐽((1st𝐺)‘𝑦)))
99 fveq2 6890 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝑥𝐵𝑋)‘𝑥) = ((𝑥𝐵𝑋)‘𝑦))
10097, 98, 99breq123d 5157 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑈𝑥)(((1st𝐹)‘𝑥)𝐽((1st𝐺)‘𝑥))((𝑥𝐵𝑋)‘𝑥) ↔ (𝑈𝑦)(((1st𝐹)‘𝑦)𝐽((1st𝐺)‘𝑦))((𝑥𝐵𝑋)‘𝑦)))
10196, 100rspc 3595 . . . . . . . . . . 11 (𝑦𝐵 → (∀𝑥𝐵 (𝑈𝑥)(((1st𝐹)‘𝑥)𝐽((1st𝐺)‘𝑥))((𝑥𝐵𝑋)‘𝑥) → (𝑈𝑦)(((1st𝐹)‘𝑦)𝐽((1st𝐺)‘𝑦))((𝑥𝐵𝑋)‘𝑦)))
10273, 45, 101sylc 65 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈𝑦)(((1st𝐹)‘𝑦)𝐽((1st𝐺)‘𝑦))((𝑥𝐵𝑋)‘𝑦))
1033, 4, 58, 74, 92, 63isinv 17768 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈𝑦)(((1st𝐹)‘𝑦)𝐽((1st𝐺)‘𝑦))((𝑥𝐵𝑋)‘𝑦) ↔ ((𝑈𝑦)(((1st𝐹)‘𝑦)(Sect‘𝐷)((1st𝐺)‘𝑦))((𝑥𝐵𝑋)‘𝑦) ∧ ((𝑥𝐵𝑋)‘𝑦)(((1st𝐺)‘𝑦)(Sect‘𝐷)((1st𝐹)‘𝑦))(𝑈𝑦))))
104102, 103mpbid 231 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈𝑦)(((1st𝐹)‘𝑦)(Sect‘𝐷)((1st𝐺)‘𝑦))((𝑥𝐵𝑋)‘𝑦) ∧ ((𝑥𝐵𝑋)‘𝑦)(((1st𝐺)‘𝑦)(Sect‘𝐷)((1st𝐹)‘𝑦))(𝑈𝑦)))
105104simprd 494 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥𝐵𝑋)‘𝑦)(((1st𝐺)‘𝑦)(Sect‘𝐷)((1st𝐹)‘𝑦))(𝑈𝑦))
1063, 21, 67, 68, 63, 58, 92, 74issect 17761 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥𝐵𝑋)‘𝑦)(((1st𝐺)‘𝑦)(Sect‘𝐷)((1st𝐹)‘𝑦))(𝑈𝑦) ↔ (((𝑥𝐵𝑋)‘𝑦) ∈ (((1st𝐺)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑦)) ∧ (𝑈𝑦) ∈ (((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐺)‘𝑦)) ∧ ((𝑈𝑦)(⟨((1st𝐺)‘𝑦), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑦))((𝑥𝐵𝑋)‘𝑦)) = ((Id‘𝐷)‘((1st𝐺)‘𝑦)))))
107105, 106mpbid 231 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥𝐵𝑋)‘𝑦) ∈ (((1st𝐺)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑦)) ∧ (𝑈𝑦) ∈ (((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐺)‘𝑦)) ∧ ((𝑈𝑦)(⟨((1st𝐺)‘𝑦), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑦))((𝑥𝐵𝑋)‘𝑦)) = ((Id‘𝐷)‘((1st𝐺)‘𝑦))))
108107simp1d 1139 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥𝐵𝑋)‘𝑦) ∈ (((1st𝐺)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
109107simp2d 1140 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈𝑦) ∈ (((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐺)‘𝑦)))
11018adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st𝐺)(𝐶 Func 𝐷)(2nd𝐺))
11110, 75, 21, 110, 73, 38funcf2 17879 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd𝐺)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st𝐺)‘𝑦)(Hom ‘𝐷)((1st𝐺)‘𝑧)))
112111, 78ffvelcdmd 7088 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd𝐺)𝑧)‘𝑓) ∈ (((1st𝐺)‘𝑦)(Hom ‘𝐷)((1st𝐺)‘𝑧)))
1133, 21, 67, 58, 74, 92, 62, 109, 112catcocl 17690 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd𝐺)𝑧)‘𝑓)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))(𝑈𝑦)) ∈ (((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐺)‘𝑧)))
1143, 21, 67, 58, 92, 74, 62, 108, 113, 60, 86catass 17691 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))(((𝑦(2nd𝐺)𝑧)‘𝑓)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))(𝑈𝑦)))(⟨((1st𝐺)‘𝑦), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥𝐵𝑋)‘𝑦)) = (((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐺)‘𝑦), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((((𝑦(2nd𝐺)𝑧)‘𝑓)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))(𝑈𝑦))(⟨((1st𝐺)‘𝑦), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))((𝑥𝐵𝑋)‘𝑦))))
11582, 84, 10, 21, 73natcl 17968 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈𝑦) ∈ (((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐺)‘𝑦)))
1163, 21, 67, 58, 92, 74, 92, 108, 115, 62, 112catass 17691 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑦(2nd𝐺)𝑧)‘𝑓)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))(𝑈𝑦))(⟨((1st𝐺)‘𝑦), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))((𝑥𝐵𝑋)‘𝑦)) = (((𝑦(2nd𝐺)𝑧)‘𝑓)(⟨((1st𝐺)‘𝑦), ((1st𝐺)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))((𝑈𝑦)(⟨((1st𝐺)‘𝑦), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑦))((𝑥𝐵𝑋)‘𝑦))))
117107simp3d 1141 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈𝑦)(⟨((1st𝐺)‘𝑦), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑦))((𝑥𝐵𝑋)‘𝑦)) = ((Id‘𝐷)‘((1st𝐺)‘𝑦)))
118117oveq2d 7429 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd𝐺)𝑧)‘𝑓)(⟨((1st𝐺)‘𝑦), ((1st𝐺)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))((𝑈𝑦)(⟨((1st𝐺)‘𝑦), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑦))((𝑥𝐵𝑋)‘𝑦))) = (((𝑦(2nd𝐺)𝑧)‘𝑓)(⟨((1st𝐺)‘𝑦), ((1st𝐺)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))((Id‘𝐷)‘((1st𝐺)‘𝑦))))
1193, 21, 68, 58, 92, 67, 62, 112catrid 17689 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd𝐺)𝑧)‘𝑓)(⟨((1st𝐺)‘𝑦), ((1st𝐺)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))((Id‘𝐷)‘((1st𝐺)‘𝑦))) = ((𝑦(2nd𝐺)𝑧)‘𝑓))
120116, 118, 1193eqtrd 2770 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑦(2nd𝐺)𝑧)‘𝑓)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))(𝑈𝑦))(⟨((1st𝐺)‘𝑦), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))((𝑥𝐵𝑋)‘𝑦)) = ((𝑦(2nd𝐺)𝑧)‘𝑓))
121120oveq2d 7429 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐺)‘𝑦), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((((𝑦(2nd𝐺)𝑧)‘𝑓)(⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))(𝑈𝑦))(⟨((1st𝐺)‘𝑦), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐺)‘𝑧))((𝑥𝐵𝑋)‘𝑦))) = (((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐺)‘𝑦), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑦(2nd𝐺)𝑧)‘𝑓)))
12291, 114, 1213eqtrrd 2771 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐺)‘𝑦), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑦(2nd𝐺)𝑧)‘𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑓)(⟨((1st𝐺)‘𝑦), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥𝐵𝑋)‘𝑦)))
123122ralrimivvva 3194 . . 3 (𝜑 → ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧)(((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐺)‘𝑦), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑦(2nd𝐺)𝑧)‘𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑓)(⟨((1st𝐺)‘𝑦), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥𝐵𝑋)‘𝑦)))
12482, 10, 75, 21, 67, 16, 5isnat2 17963 . . 3 (𝜑 → ((𝑥𝐵𝑋) ∈ (𝐺𝑁𝐹) ↔ ((𝑥𝐵𝑋) ∈ X𝑦𝐵 (((1st𝐺)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑦)) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧)(((𝑥𝐵𝑋)‘𝑧)(⟨((1st𝐺)‘𝑦), ((1st𝐺)‘𝑧)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑦(2nd𝐺)𝑧)‘𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑓)(⟨((1st𝐺)‘𝑦), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥𝐵𝑋)‘𝑦)))))
12537, 123, 124mpbir2and 711 . 2 (𝜑 → (𝑥𝐵𝑋) ∈ (𝐺𝑁𝐹))
126 nfv 1910 . . . 4 𝑦(𝑈𝑥)(((1st𝐹)‘𝑥)𝐽((1st𝐺)‘𝑥))((𝑥𝐵𝑋)‘𝑥)
127126, 96, 100cbvralw 3294 . . 3 (∀𝑥𝐵 (𝑈𝑥)(((1st𝐹)‘𝑥)𝐽((1st𝐺)‘𝑥))((𝑥𝐵𝑋)‘𝑥) ↔ ∀𝑦𝐵 (𝑈𝑦)(((1st𝐹)‘𝑦)𝐽((1st𝐺)‘𝑦))((𝑥𝐵𝑋)‘𝑦))
12844, 127sylib 217 . 2 (𝜑 → ∀𝑦𝐵 (𝑈𝑦)(((1st𝐹)‘𝑦)𝐽((1st𝐺)‘𝑦))((𝑥𝐵𝑋)‘𝑦))
129 fuciso.q . . 3 𝑄 = (𝐶 FuncCat 𝐷)
130 fucinv.i . . 3 𝐼 = (Inv‘𝑄)
131129, 10, 82, 5, 16, 130, 4fucinv 17990 . 2 (𝜑 → (𝑈(𝐹𝐼𝐺)(𝑥𝐵𝑋) ↔ (𝑈 ∈ (𝐹𝑁𝐺) ∧ (𝑥𝐵𝑋) ∈ (𝐺𝑁𝐹) ∧ ∀𝑦𝐵 (𝑈𝑦)(((1st𝐹)‘𝑦)𝐽((1st𝐺)‘𝑦))((𝑥𝐵𝑋)‘𝑦))))
1321, 125, 128, 131mpbir3and 1339 1 (𝜑𝑈(𝐹𝐼𝐺)(𝑥𝐵𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  wral 3051  Vcvv 3462  cop 4629   class class class wbr 5143  cmpt 5226   × cxp 5670  Rel wrel 5677  wf 6539  cfv 6543  (class class class)co 7413  1st c1st 7990  2nd c2nd 7991  Xcixp 8915  Basecbs 17205  Hom chom 17269  compcco 17270  Catccat 17669  Idccid 17670  Sectcsect 17752  Invcinv 17753   Func cfunc 17865   Nat cnat 17956   FuncCat cfuc 17957
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7735  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4906  df-iun 4995  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6302  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7866  df-1st 7992  df-2nd 7993  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-er 8723  df-map 8846  df-ixp 8916  df-en 8964  df-dom 8965  df-sdom 8966  df-fin 8967  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-nn 12256  df-2 12318  df-3 12319  df-4 12320  df-5 12321  df-6 12322  df-7 12323  df-8 12324  df-9 12325  df-n0 12516  df-z 12602  df-dec 12721  df-uz 12866  df-fz 13530  df-struct 17141  df-slot 17176  df-ndx 17188  df-base 17206  df-hom 17282  df-cco 17283  df-cat 17673  df-cid 17674  df-sect 17755  df-inv 17756  df-func 17869  df-nat 17958  df-fuc 17959
This theorem is referenced by:  fuciso  17992  yonedainv  18298
  Copyright terms: Public domain W3C validator