Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isomnd Structured version   Visualization version   GIF version

Theorem isomnd 32794
Description: A (left) ordered monoid is a monoid with a total ordering compatible with its operation. (Contributed by Thierry Arnoux, 30-Jan-2018.)
Hypotheses
Ref Expression
isomnd.0 𝐡 = (Baseβ€˜π‘€)
isomnd.1 + = (+gβ€˜π‘€)
isomnd.2 ≀ = (leβ€˜π‘€)
Assertion
Ref Expression
isomnd (𝑀 ∈ oMnd ↔ (𝑀 ∈ Mnd ∧ 𝑀 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐))))
Distinct variable groups:   π‘Ž,𝑏,𝑐,𝐡   𝑀,π‘Ž,𝑏,𝑐
Allowed substitution hints:   + (π‘Ž,𝑏,𝑐)   ≀ (π‘Ž,𝑏,𝑐)

Proof of Theorem isomnd
Dummy variables 𝑙 π‘š 𝑝 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvexd 6912 . . . . 5 (π‘š = 𝑀 β†’ (Baseβ€˜π‘š) ∈ V)
2 simpr 484 . . . . . . . . . . 11 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ 𝑣 = (Baseβ€˜π‘š))
3 fveq2 6897 . . . . . . . . . . . 12 (π‘š = 𝑀 β†’ (Baseβ€˜π‘š) = (Baseβ€˜π‘€))
43adantr 480 . . . . . . . . . . 11 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ (Baseβ€˜π‘š) = (Baseβ€˜π‘€))
52, 4eqtrd 2768 . . . . . . . . . 10 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ 𝑣 = (Baseβ€˜π‘€))
6 isomnd.0 . . . . . . . . . 10 𝐡 = (Baseβ€˜π‘€)
75, 6eqtr4di 2786 . . . . . . . . 9 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ 𝑣 = 𝐡)
8 raleq 3319 . . . . . . . . . . 11 (𝑣 = 𝐡 β†’ (βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)) ↔ βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))))
98raleqbi1dv 3330 . . . . . . . . . 10 (𝑣 = 𝐡 β†’ (βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)) ↔ βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))))
109raleqbi1dv 3330 . . . . . . . . 9 (𝑣 = 𝐡 β†’ (βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))))
117, 10syl 17 . . . . . . . 8 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ (βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))))
1211anbi2d 629 . . . . . . 7 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ ((π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ (π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))))
1312sbcbidv 3836 . . . . . 6 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ ([(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ [(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))))
1413sbcbidv 3836 . . . . 5 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ ([(+gβ€˜π‘š) / 𝑝][(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ [(+gβ€˜π‘š) / 𝑝][(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))))
151, 14sbcied 3822 . . . 4 (π‘š = 𝑀 β†’ ([(Baseβ€˜π‘š) / 𝑣][(+gβ€˜π‘š) / 𝑝][(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ [(+gβ€˜π‘š) / 𝑝][(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))))
16 fvexd 6912 . . . . 5 (π‘š = 𝑀 β†’ (+gβ€˜π‘š) ∈ V)
17 simpr 484 . . . . . . . . . . . . . 14 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ 𝑝 = (+gβ€˜π‘š))
18 fveq2 6897 . . . . . . . . . . . . . . 15 (π‘š = 𝑀 β†’ (+gβ€˜π‘š) = (+gβ€˜π‘€))
1918adantr 480 . . . . . . . . . . . . . 14 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ (+gβ€˜π‘š) = (+gβ€˜π‘€))
2017, 19eqtrd 2768 . . . . . . . . . . . . 13 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ 𝑝 = (+gβ€˜π‘€))
21 isomnd.1 . . . . . . . . . . . . 13 + = (+gβ€˜π‘€)
2220, 21eqtr4di 2786 . . . . . . . . . . . 12 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ 𝑝 = + )
2322oveqd 7437 . . . . . . . . . . 11 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ (π‘Žπ‘π‘) = (π‘Ž + 𝑐))
2422oveqd 7437 . . . . . . . . . . 11 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ (𝑏𝑝𝑐) = (𝑏 + 𝑐))
2523, 24breq12d 5161 . . . . . . . . . 10 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ ((π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐) ↔ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐)))
2625imbi2d 340 . . . . . . . . 9 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ ((π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)) ↔ (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐))))
2726ralbidv 3174 . . . . . . . 8 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ (βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)) ↔ βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐))))
28272ralbidv 3215 . . . . . . 7 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ (βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐))))
2928anbi2d 629 . . . . . 6 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ ((π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ (π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐)))))
3029sbcbidv 3836 . . . . 5 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ ([(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ [(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐)))))
3116, 30sbcied 3822 . . . 4 (π‘š = 𝑀 β†’ ([(+gβ€˜π‘š) / 𝑝][(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ [(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐)))))
32 fvexd 6912 . . . . . 6 (π‘š = 𝑀 β†’ (leβ€˜π‘š) ∈ V)
33 simpr 484 . . . . . . . . . . . . 13 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ 𝑙 = (leβ€˜π‘š))
34 simpl 482 . . . . . . . . . . . . . 14 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ π‘š = 𝑀)
3534fveq2d 6901 . . . . . . . . . . . . 13 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ (leβ€˜π‘š) = (leβ€˜π‘€))
3633, 35eqtrd 2768 . . . . . . . . . . . 12 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ 𝑙 = (leβ€˜π‘€))
37 isomnd.2 . . . . . . . . . . . 12 ≀ = (leβ€˜π‘€)
3836, 37eqtr4di 2786 . . . . . . . . . . 11 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ 𝑙 = ≀ )
3938breqd 5159 . . . . . . . . . 10 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ (π‘Žπ‘™π‘ ↔ π‘Ž ≀ 𝑏))
4038breqd 5159 . . . . . . . . . 10 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ ((π‘Ž + 𝑐)𝑙(𝑏 + 𝑐) ↔ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐)))
4139, 40imbi12d 344 . . . . . . . . 9 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ ((π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐)) ↔ (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐))))
4241ralbidv 3174 . . . . . . . 8 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ (βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐)) ↔ βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐))))
43422ralbidv 3215 . . . . . . 7 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ (βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐))))
4443anbi2d 629 . . . . . 6 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ ((π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐))) ↔ (π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐)))))
4532, 44sbcied 3822 . . . . 5 (π‘š = 𝑀 β†’ ([(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐))) ↔ (π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐)))))
46 eleq1 2817 . . . . . 6 (π‘š = 𝑀 β†’ (π‘š ∈ Toset ↔ 𝑀 ∈ Toset))
4746anbi1d 630 . . . . 5 (π‘š = 𝑀 β†’ ((π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐))) ↔ (𝑀 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐)))))
4845, 47bitrd 279 . . . 4 (π‘š = 𝑀 β†’ ([(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐))) ↔ (𝑀 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐)))))
4915, 31, 483bitrd 305 . . 3 (π‘š = 𝑀 β†’ ([(Baseβ€˜π‘š) / 𝑣][(+gβ€˜π‘š) / 𝑝][(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ (𝑀 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐)))))
50 df-omnd 32792 . . 3 oMnd = {π‘š ∈ Mnd ∣ [(Baseβ€˜π‘š) / 𝑣][(+gβ€˜π‘š) / 𝑝][(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))}
5149, 50elrab2 3685 . 2 (𝑀 ∈ oMnd ↔ (𝑀 ∈ Mnd ∧ (𝑀 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐)))))
52 3anass 1093 . 2 ((𝑀 ∈ Mnd ∧ 𝑀 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐))) ↔ (𝑀 ∈ Mnd ∧ (𝑀 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐)))))
5351, 52bitr4i 278 1 (𝑀 ∈ oMnd ↔ (𝑀 ∈ Mnd ∧ 𝑀 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  βˆ€wral 3058  Vcvv 3471  [wsbc 3776   class class class wbr 5148  β€˜cfv 6548  (class class class)co 7420  Basecbs 17180  +gcplusg 17233  lecple 17240  Tosetctos 18408  Mndcmnd 18694  oMndcomnd 32790
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-ext 2699  ax-nul 5306
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423  df-omnd 32792
This theorem is referenced by:  omndmnd  32797  omndtos  32798  omndadd  32799  submomnd  32803  xrge0omnd  32804  reofld  33069
  Copyright terms: Public domain W3C validator