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

Theorem ordtbaslem 21797
 Description: Lemma for ordtbas 21801. In a total order, unbounded-above intervals are closed under intersection. (Contributed by Mario Carneiro, 3-Sep-2015.)
Hypotheses
Ref Expression
ordtval.1 𝑋 = dom 𝑅
ordtval.2 𝐴 = ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})
Assertion
Ref Expression
ordtbaslem (𝑅 ∈ TosetRel → (fi‘𝐴) = 𝐴)
Distinct variable groups:   𝑥,𝑦,𝑅   𝑥,𝑋,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)

Proof of Theorem ordtbaslem
Dummy variables 𝑎 𝑏 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 3anrot 1097 . . . . . . . . . . . . 13 ((𝑦𝑋𝑎𝑋𝑏𝑋) ↔ (𝑎𝑋𝑏𝑋𝑦𝑋))
2 ordtval.1 . . . . . . . . . . . . . 14 𝑋 = dom 𝑅
32tsrlemax 17826 . . . . . . . . . . . . 13 ((𝑅 ∈ TosetRel ∧ (𝑦𝑋𝑎𝑋𝑏𝑋)) → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏)))
41, 3sylan2br 597 . . . . . . . . . . . 12 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋𝑦𝑋)) → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏)))
543exp2 1351 . . . . . . . . . . 11 (𝑅 ∈ TosetRel → (𝑎𝑋 → (𝑏𝑋 → (𝑦𝑋 → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏))))))
65imp42 430 . . . . . . . . . 10 (((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) ∧ 𝑦𝑋) → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏)))
76notbid 321 . . . . . . . . 9 (((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) ∧ 𝑦𝑋) → (¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ ¬ (𝑦𝑅𝑎𝑦𝑅𝑏)))
8 ioran 981 . . . . . . . . 9 (¬ (𝑦𝑅𝑎𝑦𝑅𝑏) ↔ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏))
97, 8syl6bb 290 . . . . . . . 8 (((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) ∧ 𝑦𝑋) → (¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)))
109rabbidva 3428 . . . . . . 7 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} = {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)})
11 ifcl 4472 . . . . . . . . 9 ((𝑏𝑋𝑎𝑋) → if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋)
1211ancoms 462 . . . . . . . 8 ((𝑎𝑋𝑏𝑋) → if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋)
13 dmexg 7598 . . . . . . . . . . . 12 (𝑅 ∈ TosetRel → dom 𝑅 ∈ V)
142, 13eqeltrid 2897 . . . . . . . . . . 11 (𝑅 ∈ TosetRel → 𝑋 ∈ V)
1514adantr 484 . . . . . . . . . 10 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → 𝑋 ∈ V)
16 rabexg 5201 . . . . . . . . . 10 (𝑋 ∈ V → {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ V)
1715, 16syl 17 . . . . . . . . 9 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ V)
1810, 17eqeltrd 2893 . . . . . . . 8 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ V)
19 eqid 2801 . . . . . . . . . 10 (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})
20 breq2 5037 . . . . . . . . . . . 12 (𝑥 = if(𝑎𝑅𝑏, 𝑏, 𝑎) → (𝑦𝑅𝑥𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)))
2120notbid 321 . . . . . . . . . . 11 (𝑥 = if(𝑎𝑅𝑏, 𝑏, 𝑎) → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)))
2221rabbidv 3430 . . . . . . . . . 10 (𝑥 = if(𝑎𝑅𝑏, 𝑏, 𝑎) → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)})
2319, 22elrnmpt1s 5797 . . . . . . . . 9 ((if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋 ∧ {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ V) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}))
24 ordtval.2 . . . . . . . . 9 𝐴 = ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})
2523, 24eleqtrrdi 2904 . . . . . . . 8 ((if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋 ∧ {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ V) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ 𝐴)
2612, 18, 25syl2an2 685 . . . . . . 7 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ 𝐴)
2710, 26eqeltrrd 2894 . . . . . 6 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴)
2827ralrimivva 3159 . . . . 5 (𝑅 ∈ TosetRel → ∀𝑎𝑋𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴)
29 rabexg 5201 . . . . . . . 8 (𝑋 ∈ V → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V)
3014, 29syl 17 . . . . . . 7 (𝑅 ∈ TosetRel → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V)
3130ralrimivw 3153 . . . . . 6 (𝑅 ∈ TosetRel → ∀𝑎𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V)
32 breq2 5037 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑦𝑅𝑥𝑦𝑅𝑎))
3332notbid 321 . . . . . . . . 9 (𝑥 = 𝑎 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅𝑎))
3433rabbidv 3430 . . . . . . . 8 (𝑥 = 𝑎 → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎})
3534cbvmptv 5136 . . . . . . 7 (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑎𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎})
36 ineq1 4134 . . . . . . . . . 10 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) = ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}))
37 inrab 4230 . . . . . . . . . 10 ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) = {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)}
3836, 37eqtrdi 2852 . . . . . . . . 9 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) = {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)})
3938eleq1d 2877 . . . . . . . 8 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → ((𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4039ralbidv 3165 . . . . . . 7 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → (∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ ∀𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4135, 40ralrnmptw 6841 . . . . . 6 (∀𝑎𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V → (∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ ∀𝑎𝑋𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4231, 41syl 17 . . . . 5 (𝑅 ∈ TosetRel → (∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ ∀𝑎𝑋𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4328, 42mpbird 260 . . . 4 (𝑅 ∈ TosetRel → ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴)
44 rabexg 5201 . . . . . . . 8 (𝑋 ∈ V → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V)
4514, 44syl 17 . . . . . . 7 (𝑅 ∈ TosetRel → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V)
4645ralrimivw 3153 . . . . . 6 (𝑅 ∈ TosetRel → ∀𝑏𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V)
47 breq2 5037 . . . . . . . . . 10 (𝑥 = 𝑏 → (𝑦𝑅𝑥𝑦𝑅𝑏))
4847notbid 321 . . . . . . . . 9 (𝑥 = 𝑏 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅𝑏))
4948rabbidv 3430 . . . . . . . 8 (𝑥 = 𝑏 → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏})
5049cbvmptv 5136 . . . . . . 7 (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑏𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏})
51 ineq2 4136 . . . . . . . 8 (𝑤 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} → (𝑧𝑤) = (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}))
5251eleq1d 2877 . . . . . . 7 (𝑤 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} → ((𝑧𝑤) ∈ 𝐴 ↔ (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5350, 52ralrnmptw 6841 . . . . . 6 (∀𝑏𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V → (∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴 ↔ ∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5446, 53syl 17 . . . . 5 (𝑅 ∈ TosetRel → (∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴 ↔ ∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5554ralbidv 3165 . . . 4 (𝑅 ∈ TosetRel → (∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴 ↔ ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5643, 55mpbird 260 . . 3 (𝑅 ∈ TosetRel → ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴)
5724raleqi 3365 . . . 4 (∀𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ ∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴)
5824, 57raleqbii 3200 . . 3 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴)
5956, 58sylibr 237 . 2 (𝑅 ∈ TosetRel → ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)
6014pwexd 5248 . . . 4 (𝑅 ∈ TosetRel → 𝒫 𝑋 ∈ V)
61 ssrab2 4010 . . . . . . . 8 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋
6214adantr 484 . . . . . . . . 9 ((𝑅 ∈ TosetRel ∧ 𝑥𝑋) → 𝑋 ∈ V)
63 elpw2g 5214 . . . . . . . . 9 (𝑋 ∈ V → ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋 ↔ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋))
6462, 63syl 17 . . . . . . . 8 ((𝑅 ∈ TosetRel ∧ 𝑥𝑋) → ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋 ↔ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋))
6561, 64mpbiri 261 . . . . . . 7 ((𝑅 ∈ TosetRel ∧ 𝑥𝑋) → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋)
6665fmpttd 6860 . . . . . 6 (𝑅 ∈ TosetRel → (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}):𝑋⟶𝒫 𝑋)
6766frnd 6498 . . . . 5 (𝑅 ∈ TosetRel → ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) ⊆ 𝒫 𝑋)
6824, 67eqsstrid 3966 . . . 4 (𝑅 ∈ TosetRel → 𝐴 ⊆ 𝒫 𝑋)
6960, 68ssexd 5195 . . 3 (𝑅 ∈ TosetRel → 𝐴 ∈ V)
70 inficl 8877 . . 3 (𝐴 ∈ V → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ (fi‘𝐴) = 𝐴))
7169, 70syl 17 . 2 (𝑅 ∈ TosetRel → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ (fi‘𝐴) = 𝐴))
7259, 71mpbid 235 1 (𝑅 ∈ TosetRel → (fi‘𝐴) = 𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2112  ∀wral 3109  {crab 3113  Vcvv 3444   ∩ cin 3883   ⊆ wss 3884  ifcif 4428  𝒫 cpw 4500   class class class wbr 5033   ↦ cmpt 5113  dom cdm 5523  ran crn 5524  ‘cfv 6328  ficfi 8862   TosetRel ctsr 17805 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-en 8497  df-fin 8500  df-fi 8863  df-ps 17806  df-tsr 17807 This theorem is referenced by:  ordtbas2  21800
 Copyright terms: Public domain W3C validator