om2noseqlt

Description: Surreal less-than relation for G . (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	om2noseq.1	$⊢ φ \to C \in No$
	om2noseq.2	$⊢ φ \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
	om2noseq.3	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), C) [ω]$
Assertion	om2noseqlt	$⊢ (φ \land (A \in ω \land B \in ω)) \to (A \in B \to G (A) <_{s} G (B))$

Proof

Step	Hyp	Ref	Expression
1		om2noseq.1	$⊢ φ \to C \in No$
2		om2noseq.2	$⊢ φ \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
3		om2noseq.3	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), C) [ω]$
4		nnaordex2	$⊢ (A \in ω \land B \in ω) \to (A \in B \leftrightarrow \exists y \in ω A +_{𝑜} suc y = B)$
5	4	adantl	$⊢ (φ \land (A \in ω \land B \in ω)) \to (A \in B \leftrightarrow \exists y \in ω A +_{𝑜} suc y = B)$
6		suceq	$⊢ y = \emptyset \to suc y = suc \emptyset$
7		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
8	6 7	eqtr4di	$⊢ y = \emptyset \to suc y = 1_{𝑜}$
9	8	oveq2d	$⊢ y = \emptyset \to A +_{𝑜} suc y = A +_{𝑜} 1_{𝑜}$
10	9	fveq2d	$⊢ y = \emptyset \to G (A +_{𝑜} suc y) = G (A +_{𝑜} 1_{𝑜})$
11	10	breq2d	$⊢ y = \emptyset \to (G (A) <_{s} G (A +_{𝑜} suc y) \leftrightarrow G (A) <_{s} G (A +_{𝑜} 1_{𝑜}))$
12		suceq	$⊢ y = z \to suc y = suc z$
13	12	oveq2d	$⊢ y = z \to A +_{𝑜} suc y = A +_{𝑜} suc z$
14	13	fveq2d	$⊢ y = z \to G (A +_{𝑜} suc y) = G (A +_{𝑜} suc z)$
15	14	breq2d	$⊢ y = z \to (G (A) <_{s} G (A +_{𝑜} suc y) \leftrightarrow G (A) <_{s} G (A +_{𝑜} suc z))$
16		suceq	$⊢ y = suc z \to suc y = suc suc z$
17	16	oveq2d	$⊢ y = suc z \to A +_{𝑜} suc y = A +_{𝑜} suc suc z$
18	17	fveq2d	$⊢ y = suc z \to G (A +_{𝑜} suc y) = G (A +_{𝑜} suc suc z)$
19	18	breq2d	$⊢ y = suc z \to (G (A) <_{s} G (A +_{𝑜} suc y) \leftrightarrow G (A) <_{s} G (A +_{𝑜} suc suc z))$
20	1 2 3	om2noseqfo	$⊢ φ \to G : ω \underset{onto}{⟶} Z$
21		fof	$⊢ G : ω \underset{onto}{⟶} Z \to G : ω ⟶ Z$
22	20 21	syl	$⊢ φ \to G : ω ⟶ Z$
23	3 1	noseqssno	$⊢ φ \to Z \subseteq No$
24	22 23	fssd	$⊢ φ \to G : ω ⟶ No$
25	24	ffvelcdmda	$⊢ (φ \land A \in ω) \to G (A) \in No$
26	25	addsridd	$⊢ (φ \land A \in ω) \to G (A) +_{s} 0_{s} = G (A)$
27		0slt1s	$⊢ 0_{s} <_{s} 1_{s}$
28		0sno	$⊢ 0_{s} \in No$
29	28	a1i	$⊢ (φ \land A \in ω) \to 0_{s} \in No$
30		1sno	$⊢ 1_{s} \in No$
31	30	a1i	$⊢ (φ \land A \in ω) \to 1_{s} \in No$
32	29 31 25	sltadd2d	$⊢ (φ \land A \in ω) \to (0_{s} <_{s} 1_{s} \leftrightarrow (G (A) +_{s} 0_{s}) <_{s} (G (A) +_{s} 1_{s}))$
33	27 32	mpbii	$⊢ (φ \land A \in ω) \to (G (A) +_{s} 0_{s}) <_{s} (G (A) +_{s} 1_{s})$
34	26 33	eqbrtrrd	$⊢ (φ \land A \in ω) \to G (A) <_{s} (G (A) +_{s} 1_{s})$
35		nnon	$⊢ A \in ω \to A \in On$
36		oa1suc	$⊢ A \in On \to A +_{𝑜} 1_{𝑜} = suc A$
37	35 36	syl	$⊢ A \in ω \to A +_{𝑜} 1_{𝑜} = suc A$
38	37	fveq2d	$⊢ A \in ω \to G (A +_{𝑜} 1_{𝑜}) = G (suc A)$
39	38	adantl	$⊢ (φ \land A \in ω) \to G (A +_{𝑜} 1_{𝑜}) = G (suc A)$
40	1	adantr	$⊢ (φ \land A \in ω) \to C \in No$
41	2	adantr	$⊢ (φ \land A \in ω) \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
42		simpr	$⊢ (φ \land A \in ω) \to A \in ω$
43	40 41 42	om2noseqsuc	$⊢ (φ \land A \in ω) \to G (suc A) = G (A) +_{s} 1_{s}$
44	39 43	eqtrd	$⊢ (φ \land A \in ω) \to G (A +_{𝑜} 1_{𝑜}) = G (A) +_{s} 1_{s}$
45	34 44	breqtrrd	$⊢ (φ \land A \in ω) \to G (A) <_{s} G (A +_{𝑜} 1_{𝑜})$
46	25	adantr	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (A) \in No$
47	24	ad2antrr	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G : ω ⟶ No$
48		peano2	$⊢ z \in ω \to suc z \in ω$
49	48	adantr	$⊢ (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z)) \to suc z \in ω$
50		nnacl	$⊢ (A \in ω \land suc z \in ω) \to A +_{𝑜} suc z \in ω$
51	42 49 50	syl2an	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to A +_{𝑜} suc z \in ω$
52	47 51	ffvelcdmd	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (A +_{𝑜} suc z) \in No$
53		peano2	$⊢ suc z \in ω \to suc suc z \in ω$
54	48 53	syl	$⊢ z \in ω \to suc suc z \in ω$
55	54	adantr	$⊢ (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z)) \to suc suc z \in ω$
56		nnacl	$⊢ (A \in ω \land suc suc z \in ω) \to A +_{𝑜} suc suc z \in ω$
57	42 55 56	syl2an	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to A +_{𝑜} suc suc z \in ω$
58	47 57	ffvelcdmd	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (A +_{𝑜} suc suc z) \in No$
59		simprr	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (A) <_{s} G (A +_{𝑜} suc z)$
60	52	addsridd	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (A +_{𝑜} suc z) +_{s} 0_{s} = G (A +_{𝑜} suc z)$
61	28	a1i	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to 0_{s} \in No$
62	30	a1i	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to 1_{s} \in No$
63	61 62 52	sltadd2d	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to (0_{s} <_{s} 1_{s} \leftrightarrow (G (A +_{𝑜} suc z) +_{s} 0_{s}) <_{s} (G (A +_{𝑜} suc z) +_{s} 1_{s}))$
64	27 63	mpbii	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to (G (A +_{𝑜} suc z) +_{s} 0_{s}) <_{s} (G (A +_{𝑜} suc z) +_{s} 1_{s})$
65	60 64	eqbrtrrd	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (A +_{𝑜} suc z) <_{s} (G (A +_{𝑜} suc z) +_{s} 1_{s})$
66		nnasuc	$⊢ (A \in ω \land suc z \in ω) \to A +_{𝑜} suc suc z = suc (A +_{𝑜} suc z)$
67	66	fveq2d	$⊢ (A \in ω \land suc z \in ω) \to G (A +_{𝑜} suc suc z) = G (suc (A +_{𝑜} suc z))$
68	42 49 67	syl2an	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (A +_{𝑜} suc suc z) = G (suc (A +_{𝑜} suc z))$
69	1	ad2antrr	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to C \in No$
70	2	ad2antrr	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
71	69 70 51	om2noseqsuc	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (suc (A +_{𝑜} suc z)) = G (A +_{𝑜} suc z) +_{s} 1_{s}$
72	68 71	eqtrd	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (A +_{𝑜} suc suc z) = G (A +_{𝑜} suc z) +_{s} 1_{s}$
73	65 72	breqtrrd	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (A +_{𝑜} suc z) <_{s} G (A +_{𝑜} suc suc z)$
74	46 52 58 59 73	slttrd	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (A) <_{s} G (A +_{𝑜} suc suc z)$
75	74	expr	$⊢ ((φ \land A \in ω) \land z \in ω) \to (G (A) <_{s} G (A +_{𝑜} suc z) \to G (A) <_{s} G (A +_{𝑜} suc suc z))$
76	75	expcom	$⊢ z \in ω \to ((φ \land A \in ω) \to (G (A) <_{s} G (A +_{𝑜} suc z) \to G (A) <_{s} G (A +_{𝑜} suc suc z)))$
77	11 15 19 45 76	finds2	$⊢ y \in ω \to ((φ \land A \in ω) \to G (A) <_{s} G (A +_{𝑜} suc y))$
78	77	impcom	$⊢ ((φ \land A \in ω) \land y \in ω) \to G (A) <_{s} G (A +_{𝑜} suc y)$
79		fveq2	$⊢ A +_{𝑜} suc y = B \to G (A +_{𝑜} suc y) = G (B)$
80	79	breq2d	$⊢ A +_{𝑜} suc y = B \to (G (A) <_{s} G (A +_{𝑜} suc y) \leftrightarrow G (A) <_{s} G (B))$
81	78 80	syl5ibcom	$⊢ ((φ \land A \in ω) \land y \in ω) \to (A +_{𝑜} suc y = B \to G (A) <_{s} G (B))$
82	81	rexlimdva	$⊢ (φ \land A \in ω) \to (\exists y \in ω A +_{𝑜} suc y = B \to G (A) <_{s} G (B))$
83	82	adantrr	$⊢ (φ \land (A \in ω \land B \in ω)) \to (\exists y \in ω A +_{𝑜} suc y = B \to G (A) <_{s} G (B))$
84	5 83	sylbid	$⊢ (φ \land (A \in ω \land B \in ω)) \to (A \in B \to G (A) <_{s} G (B))$

Metamath Proof Explorer

Theorem om2noseqlt

Proof