uzsind

Description: Induction on the upper surreal integers that start at M . (Contributed by Scott Fenton, 25-Jul-2025)

	Ref	Expression
Hypotheses	uzsind.1	$⊢ j = M \to (φ \leftrightarrow ψ)$
	uzsind.2	$⊢ j = k \to (φ \leftrightarrow χ)$
	uzsind.3	$⊢ j = k +_{s} 1_{s} \to (φ \leftrightarrow θ)$
	uzsind.4	$⊢ j = N \to (φ \leftrightarrow τ)$
	uzsind.5	$⊢ M \in ℤ_{s} \to ψ$
	uzsind.6	$⊢ (M \in ℤ_{s} \land k \in ℤ_{s} \land M \leq_{s} k) \to (χ \to θ)$
Assertion	uzsind	$⊢ (M \in ℤ_{s} \land N \in ℤ_{s} \land M \leq_{s} N) \to τ$

Proof

Step	Hyp	Ref	Expression
1		uzsind.1	$⊢ j = M \to (φ \leftrightarrow ψ)$
2		uzsind.2	$⊢ j = k \to (φ \leftrightarrow χ)$
3		uzsind.3	$⊢ j = k +_{s} 1_{s} \to (φ \leftrightarrow θ)$
4		uzsind.4	$⊢ j = N \to (φ \leftrightarrow τ)$
5		uzsind.5	$⊢ M \in ℤ_{s} \to ψ$
6		uzsind.6	$⊢ (M \in ℤ_{s} \land k \in ℤ_{s} \land M \leq_{s} k) \to (χ \to θ)$
7		id	$⊢ M \in ℤ_{s} \to M \in ℤ_{s}$
8		zno	$⊢ M \in ℤ_{s} \to M \in No$
9		slerflex	$⊢ M \in No \to M \leq_{s} M$
10	8 9	syl	$⊢ M \in ℤ_{s} \to M \leq_{s} M$
11	7 10 5	jca32	$⊢ M \in ℤ_{s} \to (M \in ℤ_{s} \land (M \leq_{s} M \land ψ))$
12		breq2	$⊢ j = M \to (M \leq_{s} j \leftrightarrow M \leq_{s} M)$
13	12 1	anbi12d	$⊢ j = M \to ((M \leq_{s} j \land φ) \leftrightarrow (M \leq_{s} M \land ψ))$
14	13	elrab	$⊢ M \in \{j \in ℤ_{s} \| (M \leq_{s} j \land φ)\} \leftrightarrow (M \in ℤ_{s} \land (M \leq_{s} M \land ψ))$
15	11 14	sylibr	$⊢ M \in ℤ_{s} \to M \in \{j \in ℤ_{s} \| (M \leq_{s} j \land φ)\}$
16		simpl	$⊢ (M \in ℤ_{s} \land (k \in ℤ_{s} \land (M \leq_{s} k \land χ))) \to M \in ℤ_{s}$
17		simprl	$⊢ (M \in ℤ_{s} \land (k \in ℤ_{s} \land (M \leq_{s} k \land χ))) \to k \in ℤ_{s}$
18		simprrl	$⊢ (M \in ℤ_{s} \land (k \in ℤ_{s} \land (M \leq_{s} k \land χ))) \to M \leq_{s} k$
19		simprrr	$⊢ (M \in ℤ_{s} \land (k \in ℤ_{s} \land (M \leq_{s} k \land χ))) \to χ$
20		id	$⊢ k \in ℤ_{s} \to k \in ℤ_{s}$
21		1zs	$⊢ 1_{s} \in ℤ_{s}$
22	21	a1i	$⊢ k \in ℤ_{s} \to 1_{s} \in ℤ_{s}$
23	20 22	zaddscld	$⊢ k \in ℤ_{s} \to k +_{s} 1_{s} \in ℤ_{s}$
24	23	3ad2ant2	$⊢ (M \in ℤ_{s} \land k \in ℤ_{s} \land M \leq_{s} k) \to k +_{s} 1_{s} \in ℤ_{s}$
25	24	adantr	$⊢ ((M \in ℤ_{s} \land k \in ℤ_{s} \land M \leq_{s} k) \land χ) \to k +_{s} 1_{s} \in ℤ_{s}$
26	8	3ad2ant1	$⊢ (M \in ℤ_{s} \land k \in ℤ_{s} \land M \leq_{s} k) \to M \in No$
27	23	znod	$⊢ k \in ℤ_{s} \to k +_{s} 1_{s} \in No$
28	27	3ad2ant2	$⊢ (M \in ℤ_{s} \land k \in ℤ_{s} \land M \leq_{s} k) \to k +_{s} 1_{s} \in No$
29		zno	$⊢ k \in ℤ_{s} \to k \in No$
30	29	3ad2ant2	$⊢ (M \in ℤ_{s} \land k \in ℤ_{s} \land M \leq_{s} k) \to k \in No$
31		simp3	$⊢ (M \in ℤ_{s} \land k \in ℤ_{s} \land M \leq_{s} k) \to M \leq_{s} k$
32	29	sltp1d	$⊢ k \in ℤ_{s} \to k <_{s} (k +_{s} 1_{s})$
33	32	3ad2ant2	$⊢ (M \in ℤ_{s} \land k \in ℤ_{s} \land M \leq_{s} k) \to k <_{s} (k +_{s} 1_{s})$
34	26 30 28 31 33	slelttrd	$⊢ (M \in ℤ_{s} \land k \in ℤ_{s} \land M \leq_{s} k) \to M <_{s} (k +_{s} 1_{s})$
35	26 28 34	sltled	$⊢ (M \in ℤ_{s} \land k \in ℤ_{s} \land M \leq_{s} k) \to M \leq_{s} (k +_{s} 1_{s})$
36	35	adantr	$⊢ ((M \in ℤ_{s} \land k \in ℤ_{s} \land M \leq_{s} k) \land χ) \to M \leq_{s} (k +_{s} 1_{s})$
37	6	imp	$⊢ ((M \in ℤ_{s} \land k \in ℤ_{s} \land M \leq_{s} k) \land χ) \to θ$
38	25 36 37	jca32	$⊢ ((M \in ℤ_{s} \land k \in ℤ_{s} \land M \leq_{s} k) \land χ) \to (k +_{s} 1_{s} \in ℤ_{s} \land (M \leq_{s} (k +_{s} 1_{s}) \land θ))$
39	16 17 18 19 38	syl31anc	$⊢ (M \in ℤ_{s} \land (k \in ℤ_{s} \land (M \leq_{s} k \land χ))) \to (k +_{s} 1_{s} \in ℤ_{s} \land (M \leq_{s} (k +_{s} 1_{s}) \land θ))$
40		breq2	$⊢ j = k \to (M \leq_{s} j \leftrightarrow M \leq_{s} k)$
41	40 2	anbi12d	$⊢ j = k \to ((M \leq_{s} j \land φ) \leftrightarrow (M \leq_{s} k \land χ))$
42	41	elrab	$⊢ k \in \{j \in ℤ_{s} \| (M \leq_{s} j \land φ)\} \leftrightarrow (k \in ℤ_{s} \land (M \leq_{s} k \land χ))$
43	42	anbi2i	$⊢ (M \in ℤ_{s} \land k \in \{j \in ℤ_{s} \| (M \leq_{s} j \land φ)\}) \leftrightarrow (M \in ℤ_{s} \land (k \in ℤ_{s} \land (M \leq_{s} k \land χ)))$
44		breq2	$⊢ j = k +_{s} 1_{s} \to (M \leq_{s} j \leftrightarrow M \leq_{s} (k +_{s} 1_{s}))$
45	44 3	anbi12d	$⊢ j = k +_{s} 1_{s} \to ((M \leq_{s} j \land φ) \leftrightarrow (M \leq_{s} (k +_{s} 1_{s}) \land θ))$
46	45	elrab	$⊢ k +_{s} 1_{s} \in \{j \in ℤ_{s} \| (M \leq_{s} j \land φ)\} \leftrightarrow (k +_{s} 1_{s} \in ℤ_{s} \land (M \leq_{s} (k +_{s} 1_{s}) \land θ))$
47	39 43 46	3imtr4i	$⊢ (M \in ℤ_{s} \land k \in \{j \in ℤ_{s} \| (M \leq_{s} j \land φ)\}) \to k +_{s} 1_{s} \in \{j \in ℤ_{s} \| (M \leq_{s} j \land φ)\}$
48	7 15 47	peano5uzs	$⊢ M \in ℤ_{s} \to \{w \in ℤ_{s} \| M \leq_{s} w\} \subseteq \{j \in ℤ_{s} \| (M \leq_{s} j \land φ)\}$
49	48	sseld	$⊢ M \in ℤ_{s} \to (N \in \{w \in ℤ_{s} \| M \leq_{s} w\} \to N \in \{j \in ℤ_{s} \| (M \leq_{s} j \land φ)\})$
50		breq2	$⊢ w = N \to (M \leq_{s} w \leftrightarrow M \leq_{s} N)$
51	50	elrab	$⊢ N \in \{w \in ℤ_{s} \| M \leq_{s} w\} \leftrightarrow (N \in ℤ_{s} \land M \leq_{s} N)$
52		breq2	$⊢ j = N \to (M \leq_{s} j \leftrightarrow M \leq_{s} N)$
53	52 4	anbi12d	$⊢ j = N \to ((M \leq_{s} j \land φ) \leftrightarrow (M \leq_{s} N \land τ))$
54	53	elrab	$⊢ N \in \{j \in ℤ_{s} \| (M \leq_{s} j \land φ)\} \leftrightarrow (N \in ℤ_{s} \land (M \leq_{s} N \land τ))$
55	49 51 54	3imtr3g	$⊢ M \in ℤ_{s} \to ((N \in ℤ_{s} \land M \leq_{s} N) \to (N \in ℤ_{s} \land (M \leq_{s} N \land τ)))$
56	55	3impib	$⊢ (M \in ℤ_{s} \land N \in ℤ_{s} \land M \leq_{s} N) \to (N \in ℤ_{s} \land (M \leq_{s} N \land τ))$
57	56	simprrd	$⊢ (M \in ℤ_{s} \land N \in ℤ_{s} \land M \leq_{s} N) \to τ$

Metamath Proof Explorer

Theorem uzsind

Proof