Theorem noinds

Description: Induction principle for a single surreal. If a property passes from a surreal's left and right sets to the surreal itself, then it holds for all surreals. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypotheses	noinds.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	noinds.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
	noinds.3	⊢ ( 𝑥 ∈ No → ( ∀ 𝑦 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜓 → 𝜑 ) )
Assertion	noinds	⊢ ( 𝐴 ∈ No → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		noinds.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		noinds.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
3		noinds.3	⊢ ( 𝑥 ∈ No → ( ∀ 𝑦 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜓 → 𝜑 ) )
4		eqid	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) }
5	4	lrrecfr	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Fr No
6	4	lrrecpo	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Po No
7	4	lrrecse	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Se No
8	5 6 7	3pm3.2i	⊢ ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Fr No ∧ { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Po No ∧ { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Se No )
9	4	lrrecpred	⊢ ( 𝑥 ∈ No → Pred ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } , No , 𝑥 ) = ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
10	9	raleqdv	⊢ ( 𝑥 ∈ No → ( ∀ 𝑦 ∈ Pred ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } , No , 𝑥 ) 𝜓 ↔ ∀ 𝑦 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜓 ) )
11	10 3	sylbid	⊢ ( 𝑥 ∈ No → ( ∀ 𝑦 ∈ Pred ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } , No , 𝑥 ) 𝜓 → 𝜑 ) )
12	11 1 2	frpoins3g	⊢ ( ( ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Fr No ∧ { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Po No ∧ { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Se No ) ∧ 𝐴 ∈ No ) → 𝜒 )
13	8 12	mpan	⊢ ( 𝐴 ∈ No → 𝜒 )