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 33866 | . . . 4 ⊢ 𝑅 Po No |
4 | 3 | a1i 11 | . . 3 ⊢ (⊤ → 𝑅 Po No ) |
5 | 1, 4, 4 | poxp2 33558 | . 2 ⊢ (⊤ → 𝑆 Po ( No × No )) |
6 | 5 | mptru 1550 | 1 ⊢ 𝑆 Po ( No × No ) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 847 ∧ w3a 1089 = wceq 1543 ⊤wtru 1544 ∈ wcel 2112 ≠ wne 2942 ∪ cun 3880 class class class wbr 5069 {copab 5131 Po wpo 5483 × cxp 5566 ‘cfv 6400 1st c1st 7780 2nd c2nd 7781 No csur 33611 L cleft 33797 R cright 33798 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-rep 5195 ax-sep 5208 ax-nul 5215 ax-pow 5274 ax-pr 5338 ax-un 7544 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3711 df-csb 3828 df-dif 3885 df-un 3887 df-in 3889 df-ss 3899 df-pss 3901 df-nul 4254 df-if 4456 df-pw 4531 df-sn 4558 df-pr 4560 df-tp 4562 df-op 4564 df-uni 4836 df-int 4876 df-iun 4922 df-br 5070 df-opab 5132 df-mpt 5152 df-tr 5178 df-id 5471 df-eprel 5477 df-po 5485 df-so 5486 df-fr 5526 df-we 5528 df-xp 5574 df-rel 5575 df-cnv 5576 df-co 5577 df-dm 5578 df-rn 5579 df-res 5580 df-ima 5581 df-pred 6178 df-ord 6236 df-on 6237 df-suc 6239 df-iota 6358 df-fun 6402 df-fn 6403 df-f 6404 df-f1 6405 df-fo 6406 df-f1o 6407 df-fv 6408 df-riota 7191 df-ov 7237 df-oprab 7238 df-mpo 7239 df-1st 7782 df-2nd 7783 df-wrecs 8070 df-recs 8131 df-1o 8225 df-2o 8226 df-no 33614 df-slt 33615 df-bday 33616 df-sslt 33744 df-scut 33746 df-made 33799 df-old 33800 df-left 33802 df-right 33803 |
This theorem is referenced by: norec2fn 33881 norec2ov 33882 |
Copyright terms: Public domain | W3C validator |