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

Theorem funcco 17864
Description: A functor maps composition in the source category to composition in the target. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
funcco.b 𝐵 = (Base‘𝐷)
funcco.h 𝐻 = (Hom ‘𝐷)
funcco.o · = (comp‘𝐷)
funcco.O 𝑂 = (comp‘𝐸)
funcco.f (𝜑𝐹(𝐷 Func 𝐸)𝐺)
funcco.x (𝜑𝑋𝐵)
funcco.y (𝜑𝑌𝐵)
funcco.z (𝜑𝑍𝐵)
funcco.m (𝜑𝑀 ∈ (𝑋𝐻𝑌))
funcco.n (𝜑𝑁 ∈ (𝑌𝐻𝑍))
Assertion
Ref Expression
funcco (𝜑 → ((𝑋𝐺𝑍)‘(𝑁(⟨𝑋, 𝑌· 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(⟨(𝐹𝑋), (𝐹𝑌)⟩𝑂(𝐹𝑍))((𝑋𝐺𝑌)‘𝑀)))

Proof of Theorem funcco
Dummy variables 𝑚 𝑛 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funcco.f . . . 4 (𝜑𝐹(𝐷 Func 𝐸)𝐺)
2 funcco.b . . . . 5 𝐵 = (Base‘𝐷)
3 eqid 2728 . . . . 5 (Base‘𝐸) = (Base‘𝐸)
4 funcco.h . . . . 5 𝐻 = (Hom ‘𝐷)
5 eqid 2728 . . . . 5 (Hom ‘𝐸) = (Hom ‘𝐸)
6 eqid 2728 . . . . 5 (Id‘𝐷) = (Id‘𝐷)
7 eqid 2728 . . . . 5 (Id‘𝐸) = (Id‘𝐸)
8 funcco.o . . . . 5 · = (comp‘𝐷)
9 funcco.O . . . . 5 𝑂 = (comp‘𝐸)
10 df-br 5153 . . . . . . . 8 (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
111, 10sylib 217 . . . . . . 7 (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
12 funcrcl 17856 . . . . . . 7 (⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
1311, 12syl 17 . . . . . 6 (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
1413simpld 493 . . . . 5 (𝜑𝐷 ∈ Cat)
1513simprd 494 . . . . 5 (𝜑𝐸 ∈ Cat)
162, 3, 4, 5, 6, 7, 8, 9, 14, 15isfunc 17857 . . . 4 (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶(Base‘𝐸) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))(Hom ‘𝐸)(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))))
171, 16mpbid 231 . . 3 (𝜑 → (𝐹:𝐵⟶(Base‘𝐸) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))(Hom ‘𝐸)(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))))
1817simp3d 1141 . 2 (𝜑 → ∀𝑥𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))
19 funcco.x . . 3 (𝜑𝑋𝐵)
20 funcco.y . . . . . 6 (𝜑𝑌𝐵)
2120adantr 479 . . . . 5 ((𝜑𝑥 = 𝑋) → 𝑌𝐵)
22 funcco.z . . . . . . 7 (𝜑𝑍𝐵)
2322ad2antrr 724 . . . . . 6 (((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑍𝐵)
24 funcco.m . . . . . . . . 9 (𝜑𝑀 ∈ (𝑋𝐻𝑌))
2524ad3antrrr 728 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑀 ∈ (𝑋𝐻𝑌))
26 simpllr 774 . . . . . . . . 9 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑥 = 𝑋)
27 simplr 767 . . . . . . . . 9 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑦 = 𝑌)
2826, 27oveq12d 7444 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌))
2925, 28eleqtrrd 2832 . . . . . . 7 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑀 ∈ (𝑥𝐻𝑦))
30 funcco.n . . . . . . . . . 10 (𝜑𝑁 ∈ (𝑌𝐻𝑍))
3130ad4antr 730 . . . . . . . . 9 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) → 𝑁 ∈ (𝑌𝐻𝑍))
32 simpllr 774 . . . . . . . . . 10 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) → 𝑦 = 𝑌)
33 simplr 767 . . . . . . . . . 10 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) → 𝑧 = 𝑍)
3432, 33oveq12d 7444 . . . . . . . . 9 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) → (𝑦𝐻𝑧) = (𝑌𝐻𝑍))
3531, 34eleqtrrd 2832 . . . . . . . 8 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) → 𝑁 ∈ (𝑦𝐻𝑧))
36 simp-5r 784 . . . . . . . . . . 11 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → 𝑥 = 𝑋)
37 simpllr 774 . . . . . . . . . . 11 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → 𝑧 = 𝑍)
3836, 37oveq12d 7444 . . . . . . . . . 10 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (𝑥𝐺𝑧) = (𝑋𝐺𝑍))
39 simp-4r 782 . . . . . . . . . . . . 13 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → 𝑦 = 𝑌)
4036, 39opeq12d 4886 . . . . . . . . . . . 12 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → ⟨𝑥, 𝑦⟩ = ⟨𝑋, 𝑌⟩)
4140, 37oveq12d 7444 . . . . . . . . . . 11 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑋, 𝑌· 𝑍))
42 simpr 483 . . . . . . . . . . 11 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁)
43 simplr 767 . . . . . . . . . . 11 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → 𝑚 = 𝑀)
4441, 42, 43oveq123d 7447 . . . . . . . . . 10 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (𝑛(⟨𝑥, 𝑦· 𝑧)𝑚) = (𝑁(⟨𝑋, 𝑌· 𝑍)𝑀))
4538, 44fveq12d 6909 . . . . . . . . 9 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = ((𝑋𝐺𝑍)‘(𝑁(⟨𝑋, 𝑌· 𝑍)𝑀)))
4636fveq2d 6906 . . . . . . . . . . . 12 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (𝐹𝑥) = (𝐹𝑋))
4739fveq2d 6906 . . . . . . . . . . . 12 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (𝐹𝑦) = (𝐹𝑌))
4846, 47opeq12d 4886 . . . . . . . . . . 11 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ = ⟨(𝐹𝑋), (𝐹𝑌)⟩)
4937fveq2d 6906 . . . . . . . . . . 11 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (𝐹𝑧) = (𝐹𝑍))
5048, 49oveq12d 7444 . . . . . . . . . 10 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧)) = (⟨(𝐹𝑋), (𝐹𝑌)⟩𝑂(𝐹𝑍)))
5139, 37oveq12d 7444 . . . . . . . . . . 11 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (𝑦𝐺𝑧) = (𝑌𝐺𝑍))
5251, 42fveq12d 6909 . . . . . . . . . 10 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → ((𝑦𝐺𝑧)‘𝑛) = ((𝑌𝐺𝑍)‘𝑁))
5336, 39oveq12d 7444 . . . . . . . . . . 11 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (𝑥𝐺𝑦) = (𝑋𝐺𝑌))
5453, 43fveq12d 6909 . . . . . . . . . 10 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → ((𝑥𝐺𝑦)‘𝑚) = ((𝑋𝐺𝑌)‘𝑀))
5550, 52, 54oveq123d 7447 . . . . . . . . 9 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)) = (((𝑌𝐺𝑍)‘𝑁)(⟨(𝐹𝑋), (𝐹𝑌)⟩𝑂(𝐹𝑍))((𝑋𝐺𝑌)‘𝑀)))
5645, 55eqeq12d 2744 . . . . . . . 8 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)) ↔ ((𝑋𝐺𝑍)‘(𝑁(⟨𝑋, 𝑌· 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(⟨(𝐹𝑋), (𝐹𝑌)⟩𝑂(𝐹𝑍))((𝑋𝐺𝑌)‘𝑀))))
5735, 56rspcdv 3603 . . . . . . 7 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) → (∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)) → ((𝑋𝐺𝑍)‘(𝑁(⟨𝑋, 𝑌· 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(⟨(𝐹𝑋), (𝐹𝑌)⟩𝑂(𝐹𝑍))((𝑋𝐺𝑌)‘𝑀))))
5829, 57rspcimdv 3601 . . . . . 6 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)) → ((𝑋𝐺𝑍)‘(𝑁(⟨𝑋, 𝑌· 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(⟨(𝐹𝑋), (𝐹𝑌)⟩𝑂(𝐹𝑍))((𝑋𝐺𝑌)‘𝑀))))
5923, 58rspcimdv 3601 . . . . 5 (((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → (∀𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)) → ((𝑋𝐺𝑍)‘(𝑁(⟨𝑋, 𝑌· 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(⟨(𝐹𝑋), (𝐹𝑌)⟩𝑂(𝐹𝑍))((𝑋𝐺𝑌)‘𝑀))))
6021, 59rspcimdv 3601 . . . 4 ((𝜑𝑥 = 𝑋) → (∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)) → ((𝑋𝐺𝑍)‘(𝑁(⟨𝑋, 𝑌· 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(⟨(𝐹𝑋), (𝐹𝑌)⟩𝑂(𝐹𝑍))((𝑋𝐺𝑌)‘𝑀))))
6160adantld 489 . . 3 ((𝜑𝑥 = 𝑋) → ((((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))) → ((𝑋𝐺𝑍)‘(𝑁(⟨𝑋, 𝑌· 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(⟨(𝐹𝑋), (𝐹𝑌)⟩𝑂(𝐹𝑍))((𝑋𝐺𝑌)‘𝑀))))
6219, 61rspcimdv 3601 . 2 (𝜑 → (∀𝑥𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))) → ((𝑋𝐺𝑍)‘(𝑁(⟨𝑋, 𝑌· 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(⟨(𝐹𝑋), (𝐹𝑌)⟩𝑂(𝐹𝑍))((𝑋𝐺𝑌)‘𝑀))))
6318, 62mpd 15 1 (𝜑 → ((𝑋𝐺𝑍)‘(𝑁(⟨𝑋, 𝑌· 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(⟨(𝐹𝑋), (𝐹𝑌)⟩𝑂(𝐹𝑍))((𝑋𝐺𝑌)‘𝑀)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3058  cop 4638   class class class wbr 5152   × cxp 5680  wf 6549  cfv 6553  (class class class)co 7426  1st c1st 7997  2nd c2nd 7998  m cmap 8851  Xcixp 8922  Basecbs 17187  Hom chom 17251  compcco 17252  Catccat 17651  Idccid 17652   Func cfunc 17847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-fv 6561  df-ov 7429  df-oprab 7430  df-mpo 7431  df-map 8853  df-ixp 8923  df-func 17851
This theorem is referenced by:  funcsect  17865  funcoppc  17868  cofucl  17881  funcres  17889  fthsect  17921  fthmon  17923  catcisolem  18106  prfcl  18201  evlfcllem  18220  curf1cl  18227  curf2cl  18230  curfcl  18231  uncfcurf  18238  yonedalem4c  18276
  Copyright terms: Public domain W3C validator