Theorem no3inds

Description: Triple induction over surreal numbers. (Contributed by Scott Fenton, 9-Oct-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.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.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 ‘ 𝑐 ) ) 𝜂 ) → 𝜑 ) )
12		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 ‘ 𝑤 ) ) ) ∧ 𝑧 ≠ 𝑤 ) ) }
13		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
14	13	lrrecfr	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } Fr No
15	13	lrrecpo	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } Po No
16	13	lrrecse	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } Se No
17	13	lrrecpred	⊢ ( 𝑎 ∈ No → Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) = ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) )
18	17	3ad2ant1	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) = ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) )
19	13	lrrecpred	⊢ ( 𝑏 ∈ No → Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) = ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) )
20	19	3ad2ant2	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) = ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) )
21	13	lrrecpred	⊢ ( 𝑐 ∈ No → Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) = ( ( L ‘ 𝑐 ) ∪ ( R ‘ 𝑐 ) ) )
22	21	3ad2ant3	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) = ( ( L ‘ 𝑐 ) ∪ ( R ‘ 𝑐 ) ) )
23	22	raleqdv	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜃 ↔ ∀ 𝑓 ∈ ( ( L ‘ 𝑐 ) ∪ ( R ‘ 𝑐 ) ) 𝜃 ) )
24	20 23	raleqbidv	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜃 ↔ ∀ 𝑒 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) ∀ 𝑓 ∈ ( ( L ‘ 𝑐 ) ∪ ( R ‘ 𝑐 ) ) 𝜃 ) )
25	18 24	raleqbidv	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜃 ↔ ∀ 𝑑 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ∀ 𝑒 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) ∀ 𝑓 ∈ ( ( L ‘ 𝑐 ) ∪ ( R ‘ 𝑐 ) ) 𝜃 ) )
26	20	raleqdv	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) 𝜒 ↔ ∀ 𝑒 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) 𝜒 ) )
27	18 26	raleqbidv	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) 𝜒 ↔ ∀ 𝑑 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ∀ 𝑒 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) 𝜒 ) )
28	22	raleqdv	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜁 ↔ ∀ 𝑓 ∈ ( ( L ‘ 𝑐 ) ∪ ( R ‘ 𝑐 ) ) 𝜁 ) )
29	18 28	raleqbidv	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜁 ↔ ∀ 𝑑 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ∀ 𝑓 ∈ ( ( L ‘ 𝑐 ) ∪ ( R ‘ 𝑐 ) ) 𝜁 ) )
30	25 27 29	3anbi123d	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ( ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜁 ) ↔ ( ∀ 𝑑 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ∀ 𝑒 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) ∀ 𝑓 ∈ ( ( L ‘ 𝑐 ) ∪ ( R ‘ 𝑐 ) ) 𝜃 ∧ ∀ 𝑑 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ∀ 𝑒 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) 𝜒 ∧ ∀ 𝑑 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ∀ 𝑓 ∈ ( ( L ‘ 𝑐 ) ∪ ( R ‘ 𝑐 ) ) 𝜁 ) ) )
31	18	raleqdv	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) 𝜓 ↔ ∀ 𝑑 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) 𝜓 ) )
32	22	raleqdv	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜏 ↔ ∀ 𝑓 ∈ ( ( L ‘ 𝑐 ) ∪ ( R ‘ 𝑐 ) ) 𝜏 ) )
33	20 32	raleqbidv	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜏 ↔ ∀ 𝑒 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) ∀ 𝑓 ∈ ( ( L ‘ 𝑐 ) ∪ ( R ‘ 𝑐 ) ) 𝜏 ) )
34	20	raleqdv	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) 𝜎 ↔ ∀ 𝑒 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) 𝜎 ) )
35	31 33 34	3anbi123d	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ( ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) 𝜎 ) ↔ ( ∀ 𝑑 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) 𝜓 ∧ ∀ 𝑒 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) ∀ 𝑓 ∈ ( ( L ‘ 𝑐 ) ∪ ( R ‘ 𝑐 ) ) 𝜏 ∧ ∀ 𝑒 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) 𝜎 ) ) )
36	22	raleqdv	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜂 ↔ ∀ 𝑓 ∈ ( ( L ‘ 𝑐 ) ∪ ( R ‘ 𝑐 ) ) 𝜂 ) )
37	30 35 36	3anbi123d	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ( ( ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , 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 ‘ 𝑐 ) ) 𝜂 ) ) )
38	37 11	sylbid	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ( ( ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) } , No , 𝑐 ) 𝜂 ) → 𝜑 ) )
39	12 14 15 16 14 15 16 14 15 16 1 2 3 4 5 6 7 8 9 10 38	xpord3ind	⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑍 ∈ No ) → 𝜆 )