Mathbox for Scott Fenton |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > noxpordpo | Structured version Visualization version GIF version |
Description: To get through most of the textbook defintions in surreal numbers we will need recursion on two variables. This set of theorems sets up the preconditions for double recursion. This theorem establishes the partial ordering. (Contributed by Scott Fenton, 19-Aug-2024.) |
Ref | Expression |
---|---|
noxpord.1 | ⊢ 𝑅 = {〈𝑎, 𝑏〉 ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))} |
noxpord.2 | ⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑅(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))} |
Ref | Expression |
---|---|
noxpordpo | ⊢ 𝑆 Po ( No × No ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | noxpord.2 | . . 3 ⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑅(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))} | |
2 | noxpord.1 | . . . . 5 ⊢ 𝑅 = {〈𝑎, 𝑏〉 ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))} | |
3 | 2 | lrrecpo 33681 | . . . 4 ⊢ 𝑅 Po No |
4 | 3 | a1i 11 | . . 3 ⊢ (⊤ → 𝑅 Po No ) |
5 | 1, 4, 4 | poxp2 33358 | . 2 ⊢ (⊤ → 𝑆 Po ( No × No )) |
6 | 5 | mptru 1545 | 1 ⊢ 𝑆 Po ( No × No ) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 844 ∧ w3a 1084 = wceq 1538 ⊤wtru 1539 ∈ wcel 2111 ≠ wne 2951 ∪ cun 3858 class class class wbr 5036 {copab 5098 Po wpo 5445 × cxp 5526 ‘cfv 6340 1st c1st 7697 2nd c2nd 7698 No csur 33441 L cleft 33624 R cright 33625 |
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 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5160 ax-sep 5173 ax-nul 5180 ax-pow 5238 ax-pr 5302 ax-un 7465 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-pss 3879 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4802 df-int 4842 df-iun 4888 df-br 5037 df-opab 5099 df-mpt 5117 df-tr 5143 df-id 5434 df-eprel 5439 df-po 5447 df-so 5448 df-fr 5487 df-we 5489 df-xp 5534 df-rel 5535 df-cnv 5536 df-co 5537 df-dm 5538 df-rn 5539 df-res 5540 df-ima 5541 df-pred 6131 df-ord 6177 df-on 6178 df-suc 6180 df-iota 6299 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-1st 7699 df-2nd 7700 df-wrecs 7963 df-recs 8024 df-1o 8118 df-2o 8119 df-no 33444 df-slt 33445 df-bday 33446 df-sslt 33574 df-scut 33576 df-made 33626 df-old 33627 df-left 33629 df-right 33630 |
This theorem is referenced by: norec2fn 33696 norec2ov 33697 |
Copyright terms: Public domain | W3C validator |