Theorem no2inds

Description: Double induction on surreals. The many substitution instances are to cover all possible cases. (Contributed by Scott Fenton, 22-Aug-2024)

	Ref	Expression
Hypotheses	no2inds.1	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
	no2inds.2	⊢ ( 𝑦 = 𝑤 → ( 𝜓 ↔ 𝜒 ) )
	no2inds.3	⊢ ( 𝑥 = 𝑧 → ( 𝜃 ↔ 𝜒 ) )
	no2inds.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
	no2inds.5	⊢ ( 𝑦 = 𝐵 → ( 𝜏 ↔ 𝜂 ) )
	no2inds.i	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ( ∀ 𝑧 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜒 ∧ ∀ 𝑧 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜓 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜃 ) → 𝜑 ) )
Assertion	no2inds	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		no2inds.1	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
2		no2inds.2	⊢ ( 𝑦 = 𝑤 → ( 𝜓 ↔ 𝜒 ) )
3		no2inds.3	⊢ ( 𝑥 = 𝑧 → ( 𝜃 ↔ 𝜒 ) )
4		no2inds.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5		no2inds.5	⊢ ( 𝑦 = 𝐵 → ( 𝜏 ↔ 𝜂 ) )
6		no2inds.i	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ( ∀ 𝑧 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜒 ∧ ∀ 𝑧 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜓 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜃 ) → 𝜑 ) )
7		eqid	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) }
8		eqid	⊢ { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( 𝑐 ∈ ( No × No ) ∧ 𝑑 ∈ ( No × No ) ∧ ( ( ( 1st ‘ 𝑐 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } ( 1st ‘ 𝑑 ) ∨ ( 1st ‘ 𝑐 ) = ( 1st ‘ 𝑑 ) ) ∧ ( ( 2nd ‘ 𝑐 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } ( 2nd ‘ 𝑑 ) ∨ ( 2nd ‘ 𝑐 ) = ( 2nd ‘ 𝑑 ) ) ∧ 𝑐 ≠ 𝑑 ) ) } = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( 𝑐 ∈ ( No × No ) ∧ 𝑑 ∈ ( No × No ) ∧ ( ( ( 1st ‘ 𝑐 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } ( 1st ‘ 𝑑 ) ∨ ( 1st ‘ 𝑐 ) = ( 1st ‘ 𝑑 ) ) ∧ ( ( 2nd ‘ 𝑐 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } ( 2nd ‘ 𝑑 ) ∨ ( 2nd ‘ 𝑐 ) = ( 2nd ‘ 𝑑 ) ) ∧ 𝑐 ≠ 𝑑 ) ) }
9	7 8 1 2 3 4 5 6	no2indslem	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝜂 )