Theorem noseqinds

Description: Induction schema for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	noseq.1	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) )
	noseq.2	⊢ ( 𝜑 → 𝐴 ∈ No )
	noseqinds.3	⊢ ( 𝑦 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
	noseqinds.4	⊢ ( 𝑦 = 𝑧 → ( 𝜓 ↔ 𝜃 ) )
	noseqinds.5	⊢ ( 𝑦 = ( 𝑧 +s 1s ) → ( 𝜓 ↔ 𝜏 ) )
	noseqinds.6	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜂 ) )
	noseqinds.7	⊢ ( 𝜑 → 𝜒 )
	noseqinds.8	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑍 ) → ( 𝜃 → 𝜏 ) )
Assertion	noseqinds	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		noseq.1	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) )
2		noseq.2	⊢ ( 𝜑 → 𝐴 ∈ No )
3		noseqinds.3	⊢ ( 𝑦 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
4		noseqinds.4	⊢ ( 𝑦 = 𝑧 → ( 𝜓 ↔ 𝜃 ) )
5		noseqinds.5	⊢ ( 𝑦 = ( 𝑧 +s 1s ) → ( 𝜓 ↔ 𝜏 ) )
6		noseqinds.6	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜂 ) )
7		noseqinds.7	⊢ ( 𝜑 → 𝜒 )
8		noseqinds.8	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑍 ) → ( 𝜃 → 𝜏 ) )
9	1 2	noseq0	⊢ ( 𝜑 → 𝐴 ∈ 𝑍 )
10	3 9 7	elrabd	⊢ ( 𝜑 → 𝐴 ∈ { 𝑦 ∈ 𝑍 ∣ 𝜓 } )
11	1	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑍 ) → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) )
12	2	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑍 ) → 𝐴 ∈ No )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑍 ) → 𝑧 ∈ 𝑍 )
14	11 12 13	noseqp1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑍 ) → ( 𝑧 +s 1s ) ∈ 𝑍 )
15	8 14	jctild	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑍 ) → ( 𝜃 → ( ( 𝑧 +s 1s ) ∈ 𝑍 ∧ 𝜏 ) ) )
16	15	expimpd	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝑍 ∧ 𝜃 ) → ( ( 𝑧 +s 1s ) ∈ 𝑍 ∧ 𝜏 ) ) )
17	4	elrab	⊢ ( 𝑧 ∈ { 𝑦 ∈ 𝑍 ∣ 𝜓 } ↔ ( 𝑧 ∈ 𝑍 ∧ 𝜃 ) )
18	5	elrab	⊢ ( ( 𝑧 +s 1s ) ∈ { 𝑦 ∈ 𝑍 ∣ 𝜓 } ↔ ( ( 𝑧 +s 1s ) ∈ 𝑍 ∧ 𝜏 ) )
19	16 17 18	3imtr4g	⊢ ( 𝜑 → ( 𝑧 ∈ { 𝑦 ∈ 𝑍 ∣ 𝜓 } → ( 𝑧 +s 1s ) ∈ { 𝑦 ∈ 𝑍 ∣ 𝜓 } ) )
20	19	imp	⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑦 ∈ 𝑍 ∣ 𝜓 } ) → ( 𝑧 +s 1s ) ∈ { 𝑦 ∈ 𝑍 ∣ 𝜓 } )
21	1 2 10 20	noseqind	⊢ ( 𝜑 → 𝑍 ⊆ { 𝑦 ∈ 𝑍 ∣ 𝜓 } )
22	21	sselda	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → 𝐵 ∈ { 𝑦 ∈ 𝑍 ∣ 𝜓 } )
23	6	elrab	⊢ ( 𝐵 ∈ { 𝑦 ∈ 𝑍 ∣ 𝜓 } ↔ ( 𝐵 ∈ 𝑍 ∧ 𝜂 ) )
24	22 23	sylib	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝐵 ∈ 𝑍 ∧ 𝜂 ) )
25	24	simprd	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → 𝜂 )