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 31958
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 6858 . . . . 5 (π‘š = 𝑀 β†’ (Baseβ€˜π‘š) ∈ V)
2 simpr 486 . . . . . . . . . . 11 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ 𝑣 = (Baseβ€˜π‘š))
3 fveq2 6843 . . . . . . . . . . . 12 (π‘š = 𝑀 β†’ (Baseβ€˜π‘š) = (Baseβ€˜π‘€))
43adantr 482 . . . . . . . . . . 11 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ (Baseβ€˜π‘š) = (Baseβ€˜π‘€))
52, 4eqtrd 2773 . . . . . . . . . 10 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ 𝑣 = (Baseβ€˜π‘€))
6 isomnd.0 . . . . . . . . . 10 𝐡 = (Baseβ€˜π‘€)
75, 6eqtr4di 2791 . . . . . . . . 9 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ 𝑣 = 𝐡)
8 raleq 3308 . . . . . . . . . . 11 (𝑣 = 𝐡 β†’ (βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)) ↔ βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))))
98raleqbi1dv 3306 . . . . . . . . . 10 (𝑣 = 𝐡 β†’ (βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)) ↔ βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))))
109raleqbi1dv 3306 . . . . . . . . 9 (𝑣 = 𝐡 β†’ (βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))))
117, 10syl 17 . . . . . . . 8 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ (βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))))
1211anbi2d 630 . . . . . . 7 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ ((π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ (π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))))
1312sbcbidv 3799 . . . . . 6 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ ([(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ [(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))))
1413sbcbidv 3799 . . . . 5 ((π‘š = 𝑀 ∧ 𝑣 = (Baseβ€˜π‘š)) β†’ ([(+gβ€˜π‘š) / 𝑝][(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ [(+gβ€˜π‘š) / 𝑝][(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))))
151, 14sbcied 3785 . . . 4 (π‘š = 𝑀 β†’ ([(Baseβ€˜π‘š) / 𝑣][(+gβ€˜π‘š) / 𝑝][(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ [(+gβ€˜π‘š) / 𝑝][(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))))
16 fvexd 6858 . . . . 5 (π‘š = 𝑀 β†’ (+gβ€˜π‘š) ∈ V)
17 simpr 486 . . . . . . . . . . . . . 14 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ 𝑝 = (+gβ€˜π‘š))
18 fveq2 6843 . . . . . . . . . . . . . . 15 (π‘š = 𝑀 β†’ (+gβ€˜π‘š) = (+gβ€˜π‘€))
1918adantr 482 . . . . . . . . . . . . . 14 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ (+gβ€˜π‘š) = (+gβ€˜π‘€))
2017, 19eqtrd 2773 . . . . . . . . . . . . 13 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ 𝑝 = (+gβ€˜π‘€))
21 isomnd.1 . . . . . . . . . . . . 13 + = (+gβ€˜π‘€)
2220, 21eqtr4di 2791 . . . . . . . . . . . 12 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ 𝑝 = + )
2322oveqd 7375 . . . . . . . . . . 11 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ (π‘Žπ‘π‘) = (π‘Ž + 𝑐))
2422oveqd 7375 . . . . . . . . . . 11 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ (𝑏𝑝𝑐) = (𝑏 + 𝑐))
2523, 24breq12d 5119 . . . . . . . . . 10 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ ((π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐) ↔ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐)))
2625imbi2d 341 . . . . . . . . 9 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ ((π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)) ↔ (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐))))
2726ralbidv 3171 . . . . . . . 8 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ (βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)) ↔ βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐))))
28272ralbidv 3209 . . . . . . 7 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ (βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐))))
2928anbi2d 630 . . . . . 6 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ ((π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ (π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐)))))
3029sbcbidv 3799 . . . . 5 ((π‘š = 𝑀 ∧ 𝑝 = (+gβ€˜π‘š)) β†’ ([(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ [(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐)))))
3116, 30sbcied 3785 . . . 4 (π‘š = 𝑀 β†’ ([(+gβ€˜π‘š) / 𝑝][(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ [(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐)))))
32 fvexd 6858 . . . . . 6 (π‘š = 𝑀 β†’ (leβ€˜π‘š) ∈ V)
33 simpr 486 . . . . . . . . . . . . 13 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ 𝑙 = (leβ€˜π‘š))
34 simpl 484 . . . . . . . . . . . . . 14 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ π‘š = 𝑀)
3534fveq2d 6847 . . . . . . . . . . . . 13 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ (leβ€˜π‘š) = (leβ€˜π‘€))
3633, 35eqtrd 2773 . . . . . . . . . . . 12 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ 𝑙 = (leβ€˜π‘€))
37 isomnd.2 . . . . . . . . . . . 12 ≀ = (leβ€˜π‘€)
3836, 37eqtr4di 2791 . . . . . . . . . . 11 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ 𝑙 = ≀ )
3938breqd 5117 . . . . . . . . . 10 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ (π‘Žπ‘™π‘ ↔ π‘Ž ≀ 𝑏))
4038breqd 5117 . . . . . . . . . 10 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ ((π‘Ž + 𝑐)𝑙(𝑏 + 𝑐) ↔ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐)))
4139, 40imbi12d 345 . . . . . . . . 9 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ ((π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐)) ↔ (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐))))
4241ralbidv 3171 . . . . . . . 8 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ (βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐)) ↔ βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐))))
43422ralbidv 3209 . . . . . . 7 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ (βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐))))
4443anbi2d 630 . . . . . 6 ((π‘š = 𝑀 ∧ 𝑙 = (leβ€˜π‘š)) β†’ ((π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐))) ↔ (π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐)))))
4532, 44sbcied 3785 . . . . 5 (π‘š = 𝑀 β†’ ([(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐))) ↔ (π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐)))))
46 eleq1 2822 . . . . . 6 (π‘š = 𝑀 β†’ (π‘š ∈ Toset ↔ 𝑀 ∈ Toset))
4746anbi1d 631 . . . . 5 (π‘š = 𝑀 β†’ ((π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐))) ↔ (𝑀 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐)))))
4845, 47bitrd 279 . . . 4 (π‘š = 𝑀 β†’ ([(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Žπ‘™π‘ β†’ (π‘Ž + 𝑐)𝑙(𝑏 + 𝑐))) ↔ (𝑀 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐)))))
4915, 31, 483bitrd 305 . . 3 (π‘š = 𝑀 β†’ ([(Baseβ€˜π‘š) / 𝑣][(+gβ€˜π‘š) / 𝑝][(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))) ↔ (𝑀 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐)))))
50 df-omnd 31956 . . 3 oMnd = {π‘š ∈ Mnd ∣ [(Baseβ€˜π‘š) / 𝑣][(+gβ€˜π‘š) / 𝑝][(leβ€˜π‘š) / 𝑙](π‘š ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))}
5149, 50elrab2 3649 . 2 (𝑀 ∈ oMnd ↔ (𝑀 ∈ Mnd ∧ (𝑀 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (π‘Ž ≀ 𝑏 β†’ (π‘Ž + 𝑐) ≀ (𝑏 + 𝑐)))))
52 3anass 1096 . 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 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3061  Vcvv 3444  [wsbc 3740   class class class wbr 5106  β€˜cfv 6497  (class class class)co 7358  Basecbs 17088  +gcplusg 17138  lecple 17145  Tosetctos 18310  Mndcmnd 18561  oMndcomnd 31954
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5264
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-ral 3062  df-rab 3407  df-v 3446  df-sbc 3741  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361  df-omnd 31956
This theorem is referenced by:  omndmnd  31961  omndtos  31962  omndadd  31963  submomnd  31967  xrge0omnd  31968  reofld  32183
  Copyright terms: Public domain W3C validator