no2indslem

Description: Double induction on surreals with explicit notation for the relationships. (Contributed by Scott Fenton, 22-Aug-2024)

	Ref	Expression
Hypotheses	no2indslem.a	⊢ 𝑅 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) }
	no2indslem.1	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
	no2indslem.2	⊢ ( 𝑦 = 𝑤 → ( 𝜓 ↔ 𝜒 ) )
	no2indslem.3	⊢ ( 𝑥 = 𝑧 → ( 𝜃 ↔ 𝜒 ) )
	no2indslem.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
	no2indslem.5	⊢ ( 𝑦 = 𝐵 → ( 𝜏 ↔ 𝜂 ) )
	no2indslem.i	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ( ∀ 𝑧 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜒 ∧ ∀ 𝑧 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜓 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜃 ) → 𝜑 ) )
Assertion	no2indslem	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		no2indslem.a	⊢ 𝑅 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) }
2		no2indslem.1	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
3		no2indslem.2	⊢ ( 𝑦 = 𝑤 → ( 𝜓 ↔ 𝜒 ) )
4		no2indslem.3	⊢ ( 𝑥 = 𝑧 → ( 𝜃 ↔ 𝜒 ) )
5		no2indslem.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
6		no2indslem.5	⊢ ( 𝑦 = 𝐵 → ( 𝜏 ↔ 𝜂 ) )
7		no2indslem.i	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ( ∀ 𝑧 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜒 ∧ ∀ 𝑧 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜓 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜃 ) → 𝜑 ) )
8	1	lrrecfr	⊢ 𝑅 Fr No
9	1	lrrecpo	⊢ 𝑅 Po No
10	1	lrrecse	⊢ 𝑅 Se No
11	1	lrrecpred	⊢ ( 𝑥 ∈ No → Pred ( 𝑅 , No , 𝑥 ) = ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
12	11	adantr	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → Pred ( 𝑅 , No , 𝑥 ) = ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
13	1	lrrecpred	⊢ ( 𝑦 ∈ No → Pred ( 𝑅 , No , 𝑦 ) = ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
14	13	adantl	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → Pred ( 𝑅 , No , 𝑦 ) = ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
15	14	raleqdv	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ∀ 𝑤 ∈ Pred ( 𝑅 , No , 𝑦 ) 𝜒 ↔ ∀ 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜒 ) )
16	12 15	raleqbidv	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ∀ 𝑧 ∈ Pred ( 𝑅 , No , 𝑥 ) ∀ 𝑤 ∈ Pred ( 𝑅 , No , 𝑦 ) 𝜒 ↔ ∀ 𝑧 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜒 ) )
17	12	raleqdv	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ∀ 𝑧 ∈ Pred ( 𝑅 , No , 𝑥 ) 𝜓 ↔ ∀ 𝑧 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜓 ) )
18	14	raleqdv	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ∀ 𝑤 ∈ Pred ( 𝑅 , No , 𝑦 ) 𝜃 ↔ ∀ 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜃 ) )
19	16 17 18	3anbi123d	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ( ∀ 𝑧 ∈ Pred ( 𝑅 , No , 𝑥 ) ∀ 𝑤 ∈ Pred ( 𝑅 , No , 𝑦 ) 𝜒 ∧ ∀ 𝑧 ∈ Pred ( 𝑅 , No , 𝑥 ) 𝜓 ∧ ∀ 𝑤 ∈ Pred ( 𝑅 , No , 𝑦 ) 𝜃 ) ↔ ( ∀ 𝑧 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜒 ∧ ∀ 𝑧 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜓 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜃 ) ) )
20	19 7	sylbid	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ( ∀ 𝑧 ∈ Pred ( 𝑅 , No , 𝑥 ) ∀ 𝑤 ∈ Pred ( 𝑅 , No , 𝑦 ) 𝜒 ∧ ∀ 𝑧 ∈ Pred ( 𝑅 , No , 𝑥 ) 𝜓 ∧ ∀ 𝑤 ∈ Pred ( 𝑅 , No , 𝑦 ) 𝜃 ) → 𝜑 ) )
21	8 9 10 8 9 10 2 3 4 5 6 20	xpord2ind	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝜂 )

Metamath Proof Explorer

Theorem no2indslem

Proof