Metamath Proof Explorer

Theorem noseqinds

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

Ref Expression
Hypotheses noseq.1 ⊢ φ → Z = rec ⁡ x ∈ V ⟼ x + s 1 s A ω
noseq.2 ⊢ φ → A ∈ No
noseqinds.3 ⊢ y = A → ψ ↔ χ
noseqinds.4 ⊢ y = z → ψ ↔ θ
noseqinds.5 ⊢ y = z + s 1 s → ψ ↔ τ
noseqinds.6 ⊢ y = B → ψ ↔ η
noseqinds.7 ⊢ φ → χ
noseqinds.8 ⊢ φ ∧ z ∈ Z → θ → τ
Assertion noseqinds ⊢ φ ∧ B ∈ Z → η

Proof

Step Hyp Ref Expression
1 noseq.1 ⊢ φ → Z = rec ⁡ x ∈ V ⟼ x + s 1 s A ω
2 noseq.2 ⊢ φ → A ∈ No
3 noseqinds.3 ⊢ y = A → ψ ↔ χ
4 noseqinds.4 ⊢ y = z → ψ ↔ θ
5 noseqinds.5 ⊢ y = z + s 1 s → ψ ↔ τ
6 noseqinds.6 ⊢ y = B → ψ ↔ η
7 noseqinds.7 ⊢ φ → χ
8 noseqinds.8 ⊢ φ ∧ z ∈ Z → θ → τ
9 1 2 noseq0 ⊢ φ → A ∈ Z
10 3 9 7 elrabd ⊢ φ → A ∈ y ∈ Z | ψ
11 1 adantr ⊢ φ ∧ z ∈ Z → Z = rec ⁡ x ∈ V ⟼ x + s 1 s A ω
12 2 adantr ⊢ φ ∧ z ∈ Z → A ∈ No
13 simpr ⊢ φ ∧ z ∈ Z → z ∈ Z
14 11 12 13 noseqp1 ⊢ φ ∧ z ∈ Z → z + s 1 s ∈ Z
15 8 14 jctild ⊢ φ ∧ z ∈ Z → θ → z + s 1 s ∈ Z ∧ τ
16 15 expimpd ⊢ φ → z ∈ Z ∧ θ → z + s 1 s ∈ Z ∧ τ
17 4 elrab ⊢ z ∈ y ∈ Z | ψ ↔ z ∈ Z ∧ θ
18 5 elrab ⊢ z + s 1 s ∈ y ∈ Z | ψ ↔ z + s 1 s ∈ Z ∧ τ
19 16 17 18 3imtr4g ⊢ φ → z ∈ y ∈ Z | ψ → z + s 1 s ∈ y ∈ Z | ψ
20 19 imp ⊢ φ ∧ z ∈ y ∈ Z | ψ → z + s 1 s ∈ y ∈ Z | ψ
21 1 2 10 20 noseqind ⊢ φ → Z ⊆ y ∈ Z | ψ
22 21 sselda ⊢ φ ∧ B ∈ Z → B ∈ y ∈ Z | ψ
23 6 elrab ⊢ B ∈ y ∈ Z | ψ ↔ B ∈ Z ∧ η
24 22 23 sylib ⊢ φ ∧ B ∈ Z → B ∈ Z ∧ η
25 24 simprd ⊢ φ ∧ B ∈ Z → η