noxpordpo - Metamath Proof Explorer

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

Theorem noxpordpo 27959

Description: To get through most of the textbook definitions 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.)

**Hypotheses**
Ref	Expression
noxpord.1	⊢ 𝑅 = {⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))}
noxpord.2	⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑅(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}

**Assertion**
Ref	Expression
noxpordpo	⊢ 𝑆 Po ( No × No )

Distinct variable groups: 𝑥,𝑅,𝑦 𝑎,𝑏 Allowed substitution hints: 𝑅(𝑎,𝑏) 𝑆(𝑥,𝑦,𝑎,𝑏)

**Proof of Theorem noxpordpo**
Step	Hyp	Ref	Expression
1		noxpord.2	. . 3 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑅(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
2		noxpord.1	. . . . 5 ⊢ 𝑅 = {⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))}
3	2	lrrecpo 27950	. . . 4 ⊢ 𝑅 Po No
4	3	a1i 11	. . 3 ⊢ (⊤ → 𝑅 Po No )
5	1, 4, 4	poxp2 8087	. 2 ⊢ (⊤ → 𝑆 Po ( No × No ))
6	5	mptru 1549	1 ⊢ 𝑆 Po ( No × No )

Colors of variables: wff setvar class

Syntax hints: ∨ wo 848 ∧ w3a 1087 = wceq 1542 ⊤wtru 1543 ∈ wcel 2114 ≠ wne 2933 ∪ cun 3888 class class class wbr 5086 {copab 5148 Po wpo 5531 × cxp 5623 ‘cfv 6493 1^st c1st 7934 2^nd c2nd 7935 No csur 27620 L cleft 27834 R cright 27835

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-1st 7936 df-2nd 7937 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-1o 8399 df-2o 8400 df-no 27623 df-lts 27624 df-bday 27625 df-slts 27767 df-cuts 27769 df-made 27836 df-old 27837 df-left 27839 df-right 27840

This theorem is referenced by: norec2fn 27965 norec2ov 27966

W3C validator