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	ltsp1d	$⊢ (φ \land A \in ω) \to G (A) <_{s} (G (A) +_{s} 1_{s})$
27		nnon	$⊢ A \in ω \to A \in On$
28		oa1suc	$⊢ A \in On \to A +_{𝑜} 1_{𝑜} = suc A$
29	27 28	syl	$⊢ A \in ω \to A +_{𝑜} 1_{𝑜} = suc A$
30	29	fveq2d	$⊢ A \in ω \to G (A +_{𝑜} 1_{𝑜}) = G (suc A)$
31	30	adantl	$⊢ (φ \land A \in ω) \to G (A +_{𝑜} 1_{𝑜}) = G (suc A)$
32	1	adantr	$⊢ (φ \land A \in ω) \to C \in No$
33	2	adantr	$⊢ (φ \land A \in ω) \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
34		simpr	$⊢ (φ \land A \in ω) \to A \in ω$
35	32 33 34	om2noseqsuc	$⊢ (φ \land A \in ω) \to G (suc A) = G (A) +_{s} 1_{s}$
36	31 35	eqtrd	$⊢ (φ \land A \in ω) \to G (A +_{𝑜} 1_{𝑜}) = G (A) +_{s} 1_{s}$
37	26 36	breqtrrd	$⊢ (φ \land A \in ω) \to G (A) <_{s} G (A +_{𝑜} 1_{𝑜})$
38	25	adantr	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (A) \in No$
39	24	ad2antrr	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G : ω ⟶ No$
40		peano2	$⊢ z \in ω \to suc z \in ω$
41	40	adantr	$⊢ (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z)) \to suc z \in ω$
42		nnacl	$⊢ (A \in ω \land suc z \in ω) \to A +_{𝑜} suc z \in ω$
43	34 41 42	syl2an	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to A +_{𝑜} suc z \in ω$
44	39 43	ffvelcdmd	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (A +_{𝑜} suc z) \in No$
45		peano2	$⊢ suc z \in ω \to suc suc z \in ω$
46	40 45	syl	$⊢ z \in ω \to suc suc z \in ω$
47	46	adantr	$⊢ (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z)) \to suc suc z \in ω$
48		nnacl	$⊢ (A \in ω \land suc suc z \in ω) \to A +_{𝑜} suc suc z \in ω$
49	34 47 48	syl2an	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to A +_{𝑜} suc suc z \in ω$
50	39 49	ffvelcdmd	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (A +_{𝑜} suc suc z) \in No$
51		simprr	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (A) <_{s} G (A +_{𝑜} suc z)$
52	44	ltsp1d	$⊢ ((φ \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})$
53		nnasuc	$⊢ (A \in ω \land suc z \in ω) \to A +_{𝑜} suc suc z = suc (A +_{𝑜} suc z)$
54	53	fveq2d	$⊢ (A \in ω \land suc z \in ω) \to G (A +_{𝑜} suc suc z) = G (suc (A +_{𝑜} suc z))$
55	34 41 54	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))$
56	1	ad2antrr	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to C \in No$
57	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) ↾}_{ω}$
58	56 57 43	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}$
59	55 58	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}$
60	52 59	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)$
61	38 44 50 51 60	ltstrd	$⊢ ((φ \land A \in ω) \land (z \in ω \land G (A) <_{s} G (A +_{𝑜} suc z))) \to G (A) <_{s} G (A +_{𝑜} suc suc z)$
62	61	expr	$⊢ ((φ \land A \in ω) \land z \in ω) \to (G (A) <_{s} G (A +_{𝑜} suc z) \to G (A) <_{s} G (A +_{𝑜} suc suc z))$
63	62	expcom	$⊢ z \in ω \to ((φ \land A \in ω) \to (G (A) <_{s} G (A +_{𝑜} suc z) \to G (A) <_{s} G (A +_{𝑜} suc suc z)))$
64	11 15 19 37 63	finds2	$⊢ y \in ω \to ((φ \land A \in ω) \to G (A) <_{s} G (A +_{𝑜} suc y))$
65	64	impcom	$⊢ ((φ \land A \in ω) \land y \in ω) \to G (A) <_{s} G (A +_{𝑜} suc y)$
66		fveq2	$⊢ A +_{𝑜} suc y = B \to G (A +_{𝑜} suc y) = G (B)$
67	66	breq2d	$⊢ A +_{𝑜} suc y = B \to (G (A) <_{s} G (A +_{𝑜} suc y) \leftrightarrow G (A) <_{s} G (B))$
68	65 67	syl5ibcom	$⊢ ((φ \land A \in ω) \land y \in ω) \to (A +_{𝑜} suc y = B \to G (A) <_{s} G (B))$
69	68	rexlimdva	$⊢ (φ \land A \in ω) \to (\exists y \in ω A +_{𝑜} suc y = B \to G (A) <_{s} G (B))$
70	69	adantrr	$⊢ (φ \land (A \in ω \land B \in ω)) \to (\exists y \in ω A +_{𝑜} suc y = B \to G (A) <_{s} G (B))$
71	5 70	sylbid	$⊢ (φ \land (A \in ω \land B \in ω)) \to (A \in B \to G (A) <_{s} G (B))$

Metamath Proof Explorer

Theorem om2noseqlt

Proof