Users' Mathboxes Mathbox for Zhi Wang < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  upciclem4 Structured version   Visualization version   GIF version

Theorem upciclem4 48899
Description: Lemma for upcic 48900 and upeu 48901. (Contributed by Zhi Wang, 19-Sep-2025.)
Hypotheses
Ref Expression
upcic.b 𝐵 = (Base‘𝐷)
upcic.c 𝐶 = (Base‘𝐸)
upcic.h 𝐻 = (Hom ‘𝐷)
upcic.j 𝐽 = (Hom ‘𝐸)
upcic.o 𝑂 = (comp‘𝐸)
upcic.f (𝜑𝐹(𝐷 Func 𝐸)𝐺)
upcic.x (𝜑𝑋𝐵)
upcic.y (𝜑𝑌𝐵)
upcic.z (𝜑𝑍𝐶)
upcic.m (𝜑𝑀 ∈ (𝑍𝐽(𝐹𝑋)))
upcic.1 (𝜑 → ∀𝑤𝐵𝑓 ∈ (𝑍𝐽(𝐹𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑤))𝑀))
upcic.n (𝜑𝑁 ∈ (𝑍𝐽(𝐹𝑌)))
upcic.2 (𝜑 → ∀𝑣𝐵𝑔 ∈ (𝑍𝐽(𝐹𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑣))𝑁))
Assertion
Ref Expression
upciclem4 (𝜑 → (𝑋( ≃𝑐𝐷)𝑌 ∧ ∃𝑟 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀)))
Distinct variable groups:   𝑣,𝐵   𝑤,𝐵   𝐷,𝑟   𝑓,𝐹,𝑘,𝑤   𝑔,𝐹,𝑙,𝑣   𝐹,𝑟   𝑓,𝐺,𝑘,𝑤   𝑔,𝐺,𝑙,𝑣   𝐺,𝑟   𝑓,𝐻,𝑘,𝑤   𝑔,𝐻,𝑙,𝑣   𝐻,𝑟   𝑓,𝐽,𝑤   𝑔,𝐽,𝑣   𝑓,𝑀,𝑘,𝑤   𝑔,𝑀,𝑙   𝑀,𝑟   𝑓,𝑁,𝑘   𝑔,𝑁,𝑙,𝑣   𝑁,𝑟   𝑓,𝑂,𝑘,𝑤   𝑔,𝑂,𝑙,𝑣   𝑂,𝑟   𝑓,𝑋,𝑘,𝑤   𝑔,𝑋,𝑙,𝑣   𝑋,𝑟   𝑓,𝑌,𝑘,𝑤   𝑔,𝑌,𝑙,𝑣   𝑌,𝑟   𝑓,𝑍,𝑘,𝑤   𝑔,𝑍,𝑙,𝑣   𝑍,𝑟
Allowed substitution hints:   𝜑(𝑤,𝑣,𝑓,𝑔,𝑘,𝑟,𝑙)   𝐵(𝑓,𝑔,𝑘,𝑟,𝑙)   𝐶(𝑤,𝑣,𝑓,𝑔,𝑘,𝑟,𝑙)   𝐷(𝑤,𝑣,𝑓,𝑔,𝑘,𝑙)   𝐸(𝑤,𝑣,𝑓,𝑔,𝑘,𝑟,𝑙)   𝐽(𝑘,𝑟,𝑙)   𝑀(𝑣)   𝑁(𝑤)

Proof of Theorem upciclem4
Dummy variables 𝑝 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 upcic.1 . . . . 5 (𝜑 → ∀𝑤𝐵𝑓 ∈ (𝑍𝐽(𝐹𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑤))𝑀))
2 upcic.y . . . . 5 (𝜑𝑌𝐵)
3 upcic.n . . . . 5 (𝜑𝑁 ∈ (𝑍𝐽(𝐹𝑌)))
41, 2, 3upciclem1 48896 . . . 4 (𝜑 → ∃!𝑝 ∈ (𝑋𝐻𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))
5 reurex 3383 . . . 4 (∃!𝑝 ∈ (𝑋𝐻𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀) → ∃𝑝 ∈ (𝑋𝐻𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))
64, 5syl 17 . . 3 (𝜑 → ∃𝑝 ∈ (𝑋𝐻𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))
7 simpl 482 . . . . 5 ((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) → 𝜑)
8 upcic.2 . . . . . 6 (𝜑 → ∀𝑣𝐵𝑔 ∈ (𝑍𝐽(𝐹𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑣))𝑁))
9 upcic.x . . . . . 6 (𝜑𝑋𝐵)
10 upcic.m . . . . . 6 (𝜑𝑀 ∈ (𝑍𝐽(𝐹𝑋)))
118, 9, 10upciclem1 48896 . . . . 5 (𝜑 → ∃!𝑞 ∈ (𝑌𝐻𝑋)𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))
12 reurex 3383 . . . . 5 (∃!𝑞 ∈ (𝑌𝐻𝑋)𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁) → ∃𝑞 ∈ (𝑌𝐻𝑋)𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))
137, 11, 123syl 18 . . . 4 ((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) → ∃𝑞 ∈ (𝑌𝐻𝑋)𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))
14 eqid 2736 . . . . 5 (Iso‘𝐷) = (Iso‘𝐷)
15 upcic.b . . . . 5 𝐵 = (Base‘𝐷)
16 upcic.f . . . . . . 7 (𝜑𝐹(𝐷 Func 𝐸)𝐺)
1716ad2antrr 726 . . . . . 6 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → 𝐹(𝐷 Func 𝐸)𝐺)
1817funcrcl2 48885 . . . . 5 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → 𝐷 ∈ Cat)
199ad2antrr 726 . . . . 5 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → 𝑋𝐵)
202ad2antrr 726 . . . . 5 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → 𝑌𝐵)
21 upcic.h . . . . . 6 𝐻 = (Hom ‘𝐷)
22 eqid 2736 . . . . . 6 (comp‘𝐷) = (comp‘𝐷)
23 eqid 2736 . . . . . 6 (Id‘𝐷) = (Id‘𝐷)
24 simplrl 777 . . . . . 6 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → 𝑝 ∈ (𝑋𝐻𝑌))
25 simprl 771 . . . . . 6 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → 𝑞 ∈ (𝑌𝐻𝑋))
26 upcic.c . . . . . . 7 𝐶 = (Base‘𝐸)
27 upcic.j . . . . . . 7 𝐽 = (Hom ‘𝐸)
28 upcic.o . . . . . . 7 𝑂 = (comp‘𝐸)
29 upcic.z . . . . . . . 8 (𝜑𝑍𝐶)
3029ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → 𝑍𝐶)
3110ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → 𝑀 ∈ (𝑍𝐽(𝐹𝑋)))
321ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → ∀𝑤𝐵𝑓 ∈ (𝑍𝐽(𝐹𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑤))𝑀))
33 simprr 773 . . . . . . 7 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))
34 simplrr 778 . . . . . . 7 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))
3515, 26, 21, 27, 28, 17, 19, 20, 30, 31, 32, 22, 24, 25, 33, 34upciclem3 48898 . . . . . 6 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → (𝑞(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑋)𝑝) = ((Id‘𝐷)‘𝑋))
363ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → 𝑁 ∈ (𝑍𝐽(𝐹𝑌)))
378ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → ∀𝑣𝐵𝑔 ∈ (𝑍𝐽(𝐹𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑣))𝑁))
3815, 26, 21, 27, 28, 17, 20, 19, 30, 36, 37, 22, 25, 24, 34, 33upciclem3 48898 . . . . . 6 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → (𝑝(⟨𝑌, 𝑋⟩(comp‘𝐷)𝑌)𝑞) = ((Id‘𝐷)‘𝑌))
3915, 21, 22, 14, 23, 18, 19, 20, 24, 25, 35, 38isisod 48883 . . . . 5 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → 𝑝 ∈ (𝑋(Iso‘𝐷)𝑌))
4014, 15, 18, 19, 20, 39brcici 17840 . . . 4 (((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) ∧ (𝑞 ∈ (𝑌𝐻𝑋) ∧ 𝑀 = (((𝑌𝐺𝑋)‘𝑞)(⟨𝑍, (𝐹𝑌)⟩𝑂(𝐹𝑋))𝑁))) → 𝑋( ≃𝑐𝐷)𝑌)
4113, 40rexlimddv 3160 . . 3 ((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) → 𝑋( ≃𝑐𝐷)𝑌)
426, 41rexlimddv 3160 . 2 (𝜑𝑋( ≃𝑐𝐷)𝑌)
4313, 39rexlimddv 3160 . . . 4 ((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) → 𝑝 ∈ (𝑋(Iso‘𝐷)𝑌))
44 simprr 773 . . . 4 ((𝜑 ∧ (𝑝 ∈ (𝑋𝐻𝑌) ∧ 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))) → 𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))
456, 43, 44reximssdv 3172 . . 3 (𝜑 → ∃𝑝 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))
46 fveq2 6904 . . . . . 6 (𝑝 = 𝑟 → ((𝑋𝐺𝑌)‘𝑝) = ((𝑋𝐺𝑌)‘𝑟))
4746oveq1d 7444 . . . . 5 (𝑝 = 𝑟 → (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀) = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))
4847eqeq2d 2747 . . . 4 (𝑝 = 𝑟 → (𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀) ↔ 𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀)))
4948cbvrexvw 3237 . . 3 (∃𝑝 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑝)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀) ↔ ∃𝑟 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))
5045, 49sylib 218 . 2 (𝜑 → ∃𝑟 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀))
5142, 50jca 511 1 (𝜑 → (𝑋( ≃𝑐𝐷)𝑌 ∧ ∃𝑟 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹𝑋)⟩𝑂(𝐹𝑌))𝑀)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  wral 3060  wrex 3069  ∃!wreu 3377  cop 4630   class class class wbr 5141  cfv 6559  (class class class)co 7429  Basecbs 17243  Hom chom 17304  compcco 17305  Idccid 17704  Isociso 17786  𝑐 ccic 17835   Func cfunc 17895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5277  ax-sep 5294  ax-nul 5304  ax-pow 5363  ax-pr 5430  ax-un 7751
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-iun 4991  df-br 5142  df-opab 5204  df-mpt 5224  df-id 5576  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-iota 6512  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-riota 7386  df-ov 7432  df-oprab 7433  df-mpo 7434  df-1st 8010  df-2nd 8011  df-supp 8182  df-map 8864  df-ixp 8934  df-cat 17707  df-cid 17708  df-sect 17787  df-inv 17788  df-iso 17789  df-cic 17836  df-func 17899
This theorem is referenced by:  upcic  48900  upeu  48901
  Copyright terms: Public domain W3C validator