Theorem no3inds

Description: Triple induction over surreal numbers. The substitution instances cover all possible instances of less than or equal to x, y, and z. (Contributed by Scott Fenton, 21-Aug-2024)

	Ref	Expression
Hypotheses	no3inds.1	⊢ ( 𝑝 = 𝑞 → ( 𝜑 ↔ 𝜓 ) )
	no3inds.2	⊢ ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜑 ↔ 𝜒 ) )
	no3inds.3	⊢ ( 𝑞 = ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ → ( 𝜓 ↔ 𝜃 ) )
	no3inds.4	⊢ ( 𝑢 = 𝑧 → ( 𝜃 ↔ 𝜏 ) )
	no3inds.5	⊢ ( 𝑡 = 𝑦 → ( 𝜃 ↔ 𝜂 ) )
	no3inds.6	⊢ ( 𝑢 = 𝑧 → ( 𝜂 ↔ 𝜁 ) )
	no3inds.7	⊢ ( 𝑤 = 𝑥 → ( 𝜃 ↔ 𝜎 ) )
	no3inds.8	⊢ ( 𝑢 = 𝑧 → ( 𝜎 ↔ 𝜌 ) )
	no3inds.9	⊢ ( 𝑡 = 𝑦 → ( 𝜎 ↔ 𝜇 ) )
	no3inds.10	⊢ ( 𝑥 = 𝐴 → ( 𝜒 ↔ 𝜆 ) )
	no3inds.11	⊢ ( 𝑦 = 𝐵 → ( 𝜆 ↔ 𝜅 ) )
	no3inds.12	⊢ ( 𝑧 = 𝐶 → ( 𝜅 ↔ 𝛻 ) )
	no3inds.i	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( ( ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜃 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜏 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜂 ) ∧ ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜁 ∧ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜎 ∧ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜌 ) ∧ ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜇 ) → 𝜒 ) )
Assertion	no3inds	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → 𝛻 )

Proof

Step	Hyp	Ref	Expression
1		no3inds.1	⊢ ( 𝑝 = 𝑞 → ( 𝜑 ↔ 𝜓 ) )
2		no3inds.2	⊢ ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜑 ↔ 𝜒 ) )
3		no3inds.3	⊢ ( 𝑞 = ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ → ( 𝜓 ↔ 𝜃 ) )
4		no3inds.4	⊢ ( 𝑢 = 𝑧 → ( 𝜃 ↔ 𝜏 ) )
5		no3inds.5	⊢ ( 𝑡 = 𝑦 → ( 𝜃 ↔ 𝜂 ) )
6		no3inds.6	⊢ ( 𝑢 = 𝑧 → ( 𝜂 ↔ 𝜁 ) )
7		no3inds.7	⊢ ( 𝑤 = 𝑥 → ( 𝜃 ↔ 𝜎 ) )
8		no3inds.8	⊢ ( 𝑢 = 𝑧 → ( 𝜎 ↔ 𝜌 ) )
9		no3inds.9	⊢ ( 𝑡 = 𝑦 → ( 𝜎 ↔ 𝜇 ) )
10		no3inds.10	⊢ ( 𝑥 = 𝐴 → ( 𝜒 ↔ 𝜆 ) )
11		no3inds.11	⊢ ( 𝑦 = 𝐵 → ( 𝜆 ↔ 𝜅 ) )
12		no3inds.12	⊢ ( 𝑧 = 𝐶 → ( 𝜅 ↔ 𝛻 ) )
13		no3inds.i	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( ( ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜃 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜏 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜂 ) ∧ ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜁 ∧ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜎 ∧ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜌 ) ∧ ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜇 ) → 𝜒 ) )
14		eqid	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) }
15		eqid	⊢ { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( 𝑐 ∈ ( ( No × No ) × No ) ∧ 𝑑 ∈ ( ( No × No ) × No ) ∧ ( ( ( ( 1st ‘ ( 1st ‘ 𝑐 ) ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } ( 1st ‘ ( 1st ‘ 𝑑 ) ) ∨ ( 1st ‘ ( 1st ‘ 𝑐 ) ) = ( 1st ‘ ( 1st ‘ 𝑑 ) ) ) ∧ ( ( 2nd ‘ ( 1st ‘ 𝑐 ) ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } ( 2nd ‘ ( 1st ‘ 𝑑 ) ) ∨ ( 2nd ‘ ( 1st ‘ 𝑐 ) ) = ( 2nd ‘ ( 1st ‘ 𝑑 ) ) ) ∧ ( ( 2nd ‘ 𝑐 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } ( 2nd ‘ 𝑑 ) ∨ ( 2nd ‘ 𝑐 ) = ( 2nd ‘ 𝑑 ) ) ) ∧ 𝑐 ≠ 𝑑 ) ) } = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( 𝑐 ∈ ( ( No × No ) × No ) ∧ 𝑑 ∈ ( ( No × No ) × No ) ∧ ( ( ( ( 1st ‘ ( 1st ‘ 𝑐 ) ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } ( 1st ‘ ( 1st ‘ 𝑑 ) ) ∨ ( 1st ‘ ( 1st ‘ 𝑐 ) ) = ( 1st ‘ ( 1st ‘ 𝑑 ) ) ) ∧ ( ( 2nd ‘ ( 1st ‘ 𝑐 ) ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } ( 2nd ‘ ( 1st ‘ 𝑑 ) ) ∨ ( 2nd ‘ ( 1st ‘ 𝑐 ) ) = ( 2nd ‘ ( 1st ‘ 𝑑 ) ) ) ∧ ( ( 2nd ‘ 𝑐 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } ( 2nd ‘ 𝑑 ) ∨ ( 2nd ‘ 𝑐 ) = ( 2nd ‘ 𝑑 ) ) ) ∧ 𝑐 ≠ 𝑑 ) ) }
16	14 15 1 2 3 4 5 6 7 8 9 10 11 12 13	no3indslem	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → 𝛻 )