Metamath Proof Explorer


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 𝜒 )