odubas - Metamath Proof Explorer

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

Theorem odubas 17601

Description: Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.)

**Hypotheses**
Ref	Expression
oduval.d	⊢ 𝐷 = (ODual‘𝑂)
odubas.b	⊢ 𝐵 = (Base‘𝑂)

**Assertion**
Ref	Expression
odubas	⊢ 𝐵 = (Base‘𝐷)

**Proof of Theorem odubas**
Step	Hyp	Ref	Expression
1		baseid 16399	. . 3 ⊢ Base = Slot (Base‘ndx)
2		1re 10439	. . . . 5 ⊢ 1 ∈ ℝ
3		1lt10 12052	. . . . 5 ⊢ 1 < ;10
4	2, 3	ltneii 10553	. . . 4 ⊢ 1 ≠ ;10
5		basendx 16403	. . . . 5 ⊢ (Base‘ndx) = 1
6		plendx 16522	. . . . 5 ⊢ (le‘ndx) = ;10
7	5, 6	neeq12i 3034	. . . 4 ⊢ ((Base‘ndx) ≠ (le‘ndx) ↔ 1 ≠ ;10)
8	4, 7	mpbir 223	. . 3 ⊢ (Base‘ndx) ≠ (le‘ndx)
9	1, 8	setsnid 16395	. 2 ⊢ (Base‘𝑂) = (Base‘(𝑂 sSet ⟨(le‘ndx), ^◡(le‘𝑂)⟩))
10		odubas.b	. 2 ⊢ 𝐵 = (Base‘𝑂)
11		oduval.d	. . . 4 ⊢ 𝐷 = (ODual‘𝑂)
12		eqid 2779	. . . 4 ⊢ (le‘𝑂) = (le‘𝑂)
13	11, 12	oduval 17598	. . 3 ⊢ 𝐷 = (𝑂 sSet ⟨(le‘ndx), ^◡(le‘𝑂)⟩)
14	13	fveq2i 6502	. 2 ⊢ (Base‘𝐷) = (Base‘(𝑂 sSet ⟨(le‘ndx), ^◡(le‘𝑂)⟩))
15	9, 10, 14	3eqtr4i 2813	1 ⊢ 𝐵 = (Base‘𝐷)

Colors of variables: wff setvar class

Syntax hints: = wceq 1507 ≠ wne 2968 ⟨cop 4447 ^◡ccnv 5406 ‘cfv 6188 (class class class)co 6976 0cc0 10335 1c1 10336 cdc 11911 ndxcnx 16336 sSet csts 16337 Basecbs 16339 lecple 16428 ODualcodu 17596

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2751 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279 ax-cnex 10391 ax-resscn 10392 ax-1cn 10393 ax-icn 10394 ax-addcl 10395 ax-addrcl 10396 ax-mulcl 10397 ax-mulrcl 10398 ax-mulcom 10399 ax-addass 10400 ax-mulass 10401 ax-distr 10402 ax-i2m1 10403 ax-1ne0 10404 ax-1rid 10405 ax-rnegex 10406 ax-rrecex 10407 ax-cnre 10408 ax-pre-lttri 10409 ax-pre-lttrn 10410 ax-pre-ltadd 10411 ax-pre-mulgt0 10412

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2760 df-cleq 2772 df-clel 2847 df-nfc 2919 df-ne 2969 df-nel 3075 df-ral 3094 df-rex 3095 df-reu 3096 df-rab 3098 df-v 3418 df-sbc 3683 df-csb 3788 df-dif 3833 df-un 3835 df-in 3837 df-ss 3844 df-pss 3846 df-nul 4180 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-tp 4446 df-op 4448 df-uni 4713 df-iun 4794 df-br 4930 df-opab 4992 df-mpt 5009 df-tr 5031 df-id 5312 df-eprel 5317 df-po 5326 df-so 5327 df-fr 5366 df-we 5368 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-pred 5986 df-ord 6032 df-on 6033 df-lim 6034 df-suc 6035 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195 df-fv 6196 df-riota 6937 df-ov 6979 df-oprab 6980 df-mpo 6981 df-om 7397 df-wrecs 7750 df-recs 7812 df-rdg 7850 df-er 8089 df-en 8307 df-dom 8308 df-sdom 8309 df-pnf 10476 df-mnf 10477 df-xr 10478 df-ltxr 10479 df-le 10480 df-sub 10672 df-neg 10673 df-nn 11440 df-2 11503 df-3 11504 df-4 11505 df-5 11506 df-6 11507 df-7 11508 df-8 11509 df-9 11510 df-dec 11912 df-ndx 16342 df-slot 16343 df-base 16345 df-sets 16346 df-ple 16441 df-odu 17597

This theorem is referenced by: odupos 17603 oduposb 17604 oduglb 17607 odulub 17609 odulatb 17611 oduclatb 17612 posglbd 17618 latmass 17656 latdisd 17658 odudlatb 17664 dlatjmdi 17665 oduprs 30372 odutos 30379 ordtcnvNEW 30804 ordtrest2NEW 30807

W3C validator