Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  funcrngcsetc Structured version   Visualization version   GIF version

Theorem funcrngcsetc 45974
Description: The "natural forgetful functor" from the category of non-unital rings into the category of sets which sends each non-unital ring to its underlying set (base set) and the morphisms (non-unital ring homomorphisms) to mappings of the corresponding base sets. An alternate proof is provided in funcrngcsetcALT 45975, using cofuval2 17700 to construct the "natural forgetful functor" from the category of non-unital rings into the category of sets by composing the "inclusion functor" from the category of non-unital rings into the category of extensible structures, see rngcifuestrc 45973, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 17964. (Contributed by AV, 26-Mar-2020.)
Hypotheses
Ref Expression
funcrngcsetc.r 𝑅 = (RngCat‘𝑈)
funcrngcsetc.s 𝑆 = (SetCat‘𝑈)
funcrngcsetc.b 𝐵 = (Base‘𝑅)
funcrngcsetc.u (𝜑𝑈 ∈ WUni)
funcrngcsetc.f (𝜑𝐹 = (𝑥𝐵 ↦ (Base‘𝑥)))
funcrngcsetc.g (𝜑𝐺 = (𝑥𝐵, 𝑦𝐵 ↦ ( I ↾ (𝑥 RngHomo 𝑦))))
Assertion
Ref Expression
funcrngcsetc (𝜑𝐹(𝑅 Func 𝑆)𝐺)
Distinct variable groups:   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆   𝑥,𝑈,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝑆(𝑦)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)

Proof of Theorem funcrngcsetc
Dummy variables 𝑎 𝑏 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2736 . . . . . 6 (ExtStrCat‘𝑈) = (ExtStrCat‘𝑈)
2 funcrngcsetc.s . . . . . 6 𝑆 = (SetCat‘𝑈)
3 eqid 2736 . . . . . 6 (Base‘(ExtStrCat‘𝑈)) = (Base‘(ExtStrCat‘𝑈))
4 eqid 2736 . . . . . 6 (Base‘𝑆) = (Base‘𝑆)
5 funcrngcsetc.u . . . . . 6 (𝜑𝑈 ∈ WUni)
61, 5estrcbas 17939 . . . . . . 7 (𝜑𝑈 = (Base‘(ExtStrCat‘𝑈)))
76mpteq1d 5188 . . . . . 6 (𝜑 → (𝑥𝑈 ↦ (Base‘𝑥)) = (𝑥 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ (Base‘𝑥)))
8 mpoeq12 7411 . . . . . . 7 ((𝑈 = (Base‘(ExtStrCat‘𝑈)) ∧ 𝑈 = (Base‘(ExtStrCat‘𝑈))) → (𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))) = (𝑥 ∈ (Base‘(ExtStrCat‘𝑈)), 𝑦 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))))
96, 6, 8syl2anc 584 . . . . . 6 (𝜑 → (𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))) = (𝑥 ∈ (Base‘(ExtStrCat‘𝑈)), 𝑦 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))))
101, 2, 3, 4, 5, 7, 9funcestrcsetc 17964 . . . . 5 (𝜑 → (𝑥𝑈 ↦ (Base‘𝑥))((ExtStrCat‘𝑈) Func 𝑆)(𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))))
11 df-br 5094 . . . . 5 ((𝑥𝑈 ↦ (Base‘𝑥))((ExtStrCat‘𝑈) Func 𝑆)(𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))) ↔ ⟨(𝑥𝑈 ↦ (Base‘𝑥)), (𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))⟩ ∈ ((ExtStrCat‘𝑈) Func 𝑆))
1210, 11sylib 217 . . . 4 (𝜑 → ⟨(𝑥𝑈 ↦ (Base‘𝑥)), (𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))⟩ ∈ ((ExtStrCat‘𝑈) Func 𝑆))
13 funcrngcsetc.r . . . . . . 7 𝑅 = (RngCat‘𝑈)
14 eqid 2736 . . . . . . 7 (Base‘𝑅) = (Base‘𝑅)
1513, 14, 5rngcbas 45941 . . . . . 6 (𝜑 → (Base‘𝑅) = (𝑈 ∩ Rng))
16 incom 4149 . . . . . 6 (𝑈 ∩ Rng) = (Rng ∩ 𝑈)
1715, 16eqtrdi 2792 . . . . 5 (𝜑 → (Base‘𝑅) = (Rng ∩ 𝑈))
18 eqid 2736 . . . . . 6 (Hom ‘𝑅) = (Hom ‘𝑅)
1913, 14, 5, 18rngchomfval 45942 . . . . 5 (𝜑 → (Hom ‘𝑅) = ( RngHomo ↾ ((Base‘𝑅) × (Base‘𝑅))))
201, 5, 17, 19rnghmsubcsetc 45953 . . . 4 (𝜑 → (Hom ‘𝑅) ∈ (Subcat‘(ExtStrCat‘𝑈)))
2112, 20funcres 17709 . . 3 (𝜑 → (⟨(𝑥𝑈 ↦ (Base‘𝑥)), (𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))⟩ ↾f (Hom ‘𝑅)) ∈ (((ExtStrCat‘𝑈) ↾cat (Hom ‘𝑅)) Func 𝑆))
22 mptexg 7154 . . . . . 6 (𝑈 ∈ WUni → (𝑥𝑈 ↦ (Base‘𝑥)) ∈ V)
235, 22syl 17 . . . . 5 (𝜑 → (𝑥𝑈 ↦ (Base‘𝑥)) ∈ V)
24 fvex 6839 . . . . . 6 (Hom ‘𝑅) ∈ V
2524a1i 11 . . . . 5 (𝜑 → (Hom ‘𝑅) ∈ V)
26 mpoexga 7987 . . . . . 6 ((𝑈 ∈ WUni ∧ 𝑈 ∈ WUni) → (𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))) ∈ V)
275, 5, 26syl2anc 584 . . . . 5 (𝜑 → (𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))) ∈ V)
2815, 19rnghmresfn 45939 . . . . 5 (𝜑 → (Hom ‘𝑅) Fn ((Base‘𝑅) × (Base‘𝑅)))
2923, 25, 27, 28resfval2 17706 . . . 4 (𝜑 → (⟨(𝑥𝑈 ↦ (Base‘𝑥)), (𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))⟩ ↾f (Hom ‘𝑅)) = ⟨((𝑥𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)), (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)))⟩)
30 inss1 4176 . . . . . . . 8 (𝑈 ∩ Rng) ⊆ 𝑈
3115, 30eqsstrdi 3986 . . . . . . 7 (𝜑 → (Base‘𝑅) ⊆ 𝑈)
3231resmptd 5981 . . . . . 6 (𝜑 → ((𝑥𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)) = (𝑥 ∈ (Base‘𝑅) ↦ (Base‘𝑥)))
33 funcrngcsetc.f . . . . . . 7 (𝜑𝐹 = (𝑥𝐵 ↦ (Base‘𝑥)))
34 funcrngcsetc.b . . . . . . . . 9 𝐵 = (Base‘𝑅)
3534a1i 11 . . . . . . . 8 (𝜑𝐵 = (Base‘𝑅))
3635mpteq1d 5188 . . . . . . 7 (𝜑 → (𝑥𝐵 ↦ (Base‘𝑥)) = (𝑥 ∈ (Base‘𝑅) ↦ (Base‘𝑥)))
3733, 36eqtr2d 2777 . . . . . 6 (𝜑 → (𝑥 ∈ (Base‘𝑅) ↦ (Base‘𝑥)) = 𝐹)
3832, 37eqtrd 2776 . . . . 5 (𝜑 → ((𝑥𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)) = 𝐹)
39 funcrngcsetc.g . . . . . 6 (𝜑𝐺 = (𝑥𝐵, 𝑦𝐵 ↦ ( I ↾ (𝑥 RngHomo 𝑦))))
40 oveq1 7345 . . . . . . . . 9 (𝑥 = 𝑎 → (𝑥 RngHomo 𝑦) = (𝑎 RngHomo 𝑦))
4140reseq2d 5924 . . . . . . . 8 (𝑥 = 𝑎 → ( I ↾ (𝑥 RngHomo 𝑦)) = ( I ↾ (𝑎 RngHomo 𝑦)))
42 oveq2 7346 . . . . . . . . 9 (𝑦 = 𝑏 → (𝑎 RngHomo 𝑦) = (𝑎 RngHomo 𝑏))
4342reseq2d 5924 . . . . . . . 8 (𝑦 = 𝑏 → ( I ↾ (𝑎 RngHomo 𝑦)) = ( I ↾ (𝑎 RngHomo 𝑏)))
4441, 43cbvmpov 7433 . . . . . . 7 (𝑥𝐵, 𝑦𝐵 ↦ ( I ↾ (𝑥 RngHomo 𝑦))) = (𝑎𝐵, 𝑏𝐵 ↦ ( I ↾ (𝑎 RngHomo 𝑏)))
4544a1i 11 . . . . . 6 (𝜑 → (𝑥𝐵, 𝑦𝐵 ↦ ( I ↾ (𝑥 RngHomo 𝑦))) = (𝑎𝐵, 𝑏𝐵 ↦ ( I ↾ (𝑎 RngHomo 𝑏))))
4634a1i 11 . . . . . . 7 ((𝜑𝑎𝐵) → 𝐵 = (Base‘𝑅))
47 eqidd 2737 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → (𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))) = (𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥)))))
48 fveq2 6826 . . . . . . . . . . . . 13 (𝑦 = 𝑏 → (Base‘𝑦) = (Base‘𝑏))
49 fveq2 6826 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (Base‘𝑥) = (Base‘𝑎))
5048, 49oveqan12rd 7358 . . . . . . . . . . . 12 ((𝑥 = 𝑎𝑦 = 𝑏) → ((Base‘𝑦) ↑m (Base‘𝑥)) = ((Base‘𝑏) ↑m (Base‘𝑎)))
5150reseq2d 5924 . . . . . . . . . . 11 ((𝑥 = 𝑎𝑦 = 𝑏) → ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))) = ( I ↾ ((Base‘𝑏) ↑m (Base‘𝑎))))
5251adantl 482 . . . . . . . . . 10 (((𝜑 ∧ (𝑎𝐵𝑏𝐵)) ∧ (𝑥 = 𝑎𝑦 = 𝑏)) → ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))) = ( I ↾ ((Base‘𝑏) ↑m (Base‘𝑎))))
5334, 31eqsstrid 3980 . . . . . . . . . . . . . 14 (𝜑𝐵𝑈)
5453sseld 3931 . . . . . . . . . . . . 13 (𝜑 → (𝑎𝐵𝑎𝑈))
5554com12 32 . . . . . . . . . . . 12 (𝑎𝐵 → (𝜑𝑎𝑈))
5655adantr 481 . . . . . . . . . . 11 ((𝑎𝐵𝑏𝐵) → (𝜑𝑎𝑈))
5756impcom 408 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → 𝑎𝑈)
5853sseld 3931 . . . . . . . . . . . 12 (𝜑 → (𝑏𝐵𝑏𝑈))
5958adantld 491 . . . . . . . . . . 11 (𝜑 → ((𝑎𝐵𝑏𝐵) → 𝑏𝑈))
6059imp 407 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → 𝑏𝑈)
61 ovexd 7373 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → ((Base‘𝑏) ↑m (Base‘𝑎)) ∈ V)
6261resiexd 7149 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → ( I ↾ ((Base‘𝑏) ↑m (Base‘𝑎))) ∈ V)
6347, 52, 57, 60, 62ovmpod 7488 . . . . . . . . 9 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → (𝑎(𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))𝑏) = ( I ↾ ((Base‘𝑏) ↑m (Base‘𝑎))))
6463reseq1d 5923 . . . . . . . 8 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → ((𝑎(𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)) = (( I ↾ ((Base‘𝑏) ↑m (Base‘𝑎))) ↾ (𝑎(Hom ‘𝑅)𝑏)))
655adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → 𝑈 ∈ WUni)
66 simprl 768 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → 𝑎𝐵)
67 simprr 770 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → 𝑏𝐵)
6813, 34, 65, 18, 66, 67rngchom 45943 . . . . . . . . 9 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → (𝑎(Hom ‘𝑅)𝑏) = (𝑎 RngHomo 𝑏))
6968reseq2d 5924 . . . . . . . 8 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → (( I ↾ ((Base‘𝑏) ↑m (Base‘𝑎))) ↾ (𝑎(Hom ‘𝑅)𝑏)) = (( I ↾ ((Base‘𝑏) ↑m (Base‘𝑎))) ↾ (𝑎 RngHomo 𝑏)))
70 eqid 2736 . . . . . . . . . . . 12 (Base‘𝑎) = (Base‘𝑎)
71 eqid 2736 . . . . . . . . . . . 12 (Base‘𝑏) = (Base‘𝑏)
7270, 71rnghmf 45875 . . . . . . . . . . 11 (𝑓 ∈ (𝑎 RngHomo 𝑏) → 𝑓:(Base‘𝑎)⟶(Base‘𝑏))
73 fvex 6839 . . . . . . . . . . . . . 14 (Base‘𝑏) ∈ V
74 fvex 6839 . . . . . . . . . . . . . 14 (Base‘𝑎) ∈ V
7573, 74pm3.2i 471 . . . . . . . . . . . . 13 ((Base‘𝑏) ∈ V ∧ (Base‘𝑎) ∈ V)
7675a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → ((Base‘𝑏) ∈ V ∧ (Base‘𝑎) ∈ V))
77 elmapg 8700 . . . . . . . . . . . 12 (((Base‘𝑏) ∈ V ∧ (Base‘𝑎) ∈ V) → (𝑓 ∈ ((Base‘𝑏) ↑m (Base‘𝑎)) ↔ 𝑓:(Base‘𝑎)⟶(Base‘𝑏)))
7876, 77syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → (𝑓 ∈ ((Base‘𝑏) ↑m (Base‘𝑎)) ↔ 𝑓:(Base‘𝑎)⟶(Base‘𝑏)))
7972, 78syl5ibr 245 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → (𝑓 ∈ (𝑎 RngHomo 𝑏) → 𝑓 ∈ ((Base‘𝑏) ↑m (Base‘𝑎))))
8079ssrdv 3938 . . . . . . . . 9 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → (𝑎 RngHomo 𝑏) ⊆ ((Base‘𝑏) ↑m (Base‘𝑎)))
8180resabs1d 5955 . . . . . . . 8 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → (( I ↾ ((Base‘𝑏) ↑m (Base‘𝑎))) ↾ (𝑎 RngHomo 𝑏)) = ( I ↾ (𝑎 RngHomo 𝑏)))
8264, 69, 813eqtrrd 2781 . . . . . . 7 ((𝜑 ∧ (𝑎𝐵𝑏𝐵)) → ( I ↾ (𝑎 RngHomo 𝑏)) = ((𝑎(𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)))
8335, 46, 82mpoeq123dva 7412 . . . . . 6 (𝜑 → (𝑎𝐵, 𝑏𝐵 ↦ ( I ↾ (𝑎 RngHomo 𝑏))) = (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏))))
8439, 45, 833eqtrrd 2781 . . . . 5 (𝜑 → (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏))) = 𝐺)
8538, 84opeq12d 4826 . . . 4 (𝜑 → ⟨((𝑥𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)), (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)))⟩ = ⟨𝐹, 𝐺⟩)
8629, 85eqtr2d 2777 . . 3 (𝜑 → ⟨𝐹, 𝐺⟩ = (⟨(𝑥𝑈 ↦ (Base‘𝑥)), (𝑥𝑈, 𝑦𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))⟩ ↾f (Hom ‘𝑅)))
8713, 5, 15, 19rngcval 45938 . . . 4 (𝜑𝑅 = ((ExtStrCat‘𝑈) ↾cat (Hom ‘𝑅)))
8887oveq1d 7353 . . 3 (𝜑 → (𝑅 Func 𝑆) = (((ExtStrCat‘𝑈) ↾cat (Hom ‘𝑅)) Func 𝑆))
8921, 86, 883eltr4d 2852 . 2 (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑅 Func 𝑆))
90 df-br 5094 . 2 (𝐹(𝑅 Func 𝑆)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝑅 Func 𝑆))
9189, 90sylibr 233 1 (𝜑𝐹(𝑅 Func 𝑆)𝐺)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  Vcvv 3441  cin 3897  cop 4580   class class class wbr 5093  cmpt 5176   I cid 5518  cres 5623  wf 6476  cfv 6480  (class class class)co 7338  cmpo 7340  m cmap 8687  WUnicwun 10558  Basecbs 17010  Hom chom 17071  cat cresc 17618   Func cfunc 17667  f cresf 17670  SetCatcsetc 17888  ExtStrCatcestrc 17936  Rngcrng 45850   RngHomo crngh 45861  RngCatcrngc 45933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-cnex 11029  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049  ax-pre-mulgt0 11050
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-tp 4579  df-op 4581  df-uni 4854  df-iun 4944  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-om 7782  df-1st 7900  df-2nd 7901  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-1o 8368  df-er 8570  df-map 8689  df-pm 8690  df-ixp 8758  df-en 8806  df-dom 8807  df-sdom 8808  df-fin 8809  df-wun 10560  df-pnf 11113  df-mnf 11114  df-xr 11115  df-ltxr 11116  df-le 11117  df-sub 11309  df-neg 11310  df-nn 12076  df-2 12138  df-3 12139  df-4 12140  df-5 12141  df-6 12142  df-7 12143  df-8 12144  df-9 12145  df-n0 12336  df-z 12422  df-dec 12540  df-uz 12685  df-fz 13342  df-struct 16946  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040  df-plusg 17073  df-hom 17084  df-cco 17085  df-0g 17250  df-cat 17475  df-cid 17476  df-homf 17477  df-ssc 17620  df-resc 17621  df-subc 17622  df-func 17671  df-resf 17674  df-setc 17889  df-estrc 17937  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-mhm 18528  df-grp 18677  df-ghm 18929  df-abl 19485  df-mgp 19817  df-mgmhm 45751  df-rng0 45851  df-rnghomo 45863  df-rngc 45935
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator