Theorem on3ind

Description: Triple induction over ordinals. (Contributed by Scott Fenton, 4-Sep-2024)

	Ref	Expression
Hypotheses	on3ind.1	⊢ ( 𝑎 = 𝑑 → ( 𝜑 ↔ 𝜓 ) )
	on3ind.2	⊢ ( 𝑏 = 𝑒 → ( 𝜓 ↔ 𝜒 ) )
	on3ind.3	⊢ ( 𝑐 = 𝑓 → ( 𝜒 ↔ 𝜃 ) )
	on3ind.4	⊢ ( 𝑎 = 𝑑 → ( 𝜏 ↔ 𝜃 ) )
	on3ind.5	⊢ ( 𝑏 = 𝑒 → ( 𝜂 ↔ 𝜏 ) )
	on3ind.6	⊢ ( 𝑏 = 𝑒 → ( 𝜁 ↔ 𝜃 ) )
	on3ind.7	⊢ ( 𝑐 = 𝑓 → ( 𝜎 ↔ 𝜏 ) )
	on3ind.8	⊢ ( 𝑎 = 𝑋 → ( 𝜑 ↔ 𝜌 ) )
	on3ind.9	⊢ ( 𝑏 = 𝑌 → ( 𝜌 ↔ 𝜇 ) )
	on3ind.10	⊢ ( 𝑐 = 𝑍 → ( 𝜇 ↔ 𝜆 ) )
	on3ind.i	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ( ( ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜃 ∧ ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 𝜒 ∧ ∀ 𝑑 ∈ 𝑎 ∀ 𝑓 ∈ 𝑐 𝜁 ) ∧ ( ∀ 𝑑 ∈ 𝑎 𝜓 ∧ ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜏 ∧ ∀ 𝑒 ∈ 𝑏 𝜎 ) ∧ ∀ 𝑓 ∈ 𝑐 𝜂 ) → 𝜑 ) )
Assertion	on3ind	⊢ ( ( 𝑋 ∈ On ∧ 𝑌 ∈ On ∧ 𝑍 ∈ On ) → 𝜆 )

Proof

Step	Hyp	Ref	Expression
1		on3ind.1	⊢ ( 𝑎 = 𝑑 → ( 𝜑 ↔ 𝜓 ) )
2		on3ind.2	⊢ ( 𝑏 = 𝑒 → ( 𝜓 ↔ 𝜒 ) )
3		on3ind.3	⊢ ( 𝑐 = 𝑓 → ( 𝜒 ↔ 𝜃 ) )
4		on3ind.4	⊢ ( 𝑎 = 𝑑 → ( 𝜏 ↔ 𝜃 ) )
5		on3ind.5	⊢ ( 𝑏 = 𝑒 → ( 𝜂 ↔ 𝜏 ) )
6		on3ind.6	⊢ ( 𝑏 = 𝑒 → ( 𝜁 ↔ 𝜃 ) )
7		on3ind.7	⊢ ( 𝑐 = 𝑓 → ( 𝜎 ↔ 𝜏 ) )
8		on3ind.8	⊢ ( 𝑎 = 𝑋 → ( 𝜑 ↔ 𝜌 ) )
9		on3ind.9	⊢ ( 𝑏 = 𝑌 → ( 𝜌 ↔ 𝜇 ) )
10		on3ind.10	⊢ ( 𝑐 = 𝑍 → ( 𝜇 ↔ 𝜆 ) )
11		on3ind.i	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ( ( ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜃 ∧ ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 𝜒 ∧ ∀ 𝑑 ∈ 𝑎 ∀ 𝑓 ∈ 𝑐 𝜁 ) ∧ ( ∀ 𝑑 ∈ 𝑎 𝜓 ∧ ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜏 ∧ ∀ 𝑒 ∈ 𝑏 𝜎 ) ∧ ∀ 𝑓 ∈ 𝑐 𝜂 ) → 𝜑 ) )
12		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( On × On ) × On ) ∧ 𝑦 ∈ ( ( On × On ) × On ) ∧ ( ( ( ( 1st ‘ ( 1st ‘ 𝑥 ) ) E ( 1st ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 1st ‘ ( 1st ‘ 𝑥 ) ) = ( 1st ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ ( 1st ‘ 𝑥 ) ) E ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 2nd ‘ ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ 𝑥 ) E ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( On × On ) × On ) ∧ 𝑦 ∈ ( ( On × On ) × On ) ∧ ( ( ( ( 1st ‘ ( 1st ‘ 𝑥 ) ) E ( 1st ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 1st ‘ ( 1st ‘ 𝑥 ) ) = ( 1st ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ ( 1st ‘ 𝑥 ) ) E ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 2nd ‘ ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ 𝑥 ) E ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
13		onfr	⊢ E Fr On
14		epweon	⊢ E We On
15		weso	⊢ ( E We On → E Or On )
16		sopo	⊢ ( E Or On → E Po On )
17	14 15 16	mp2b	⊢ E Po On
18		epse	⊢ E Se On
19		predon	⊢ ( 𝑎 ∈ On → Pred ( E , On , 𝑎 ) = 𝑎 )
20	19	3ad2ant1	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → Pred ( E , On , 𝑎 ) = 𝑎 )
21		predon	⊢ ( 𝑏 ∈ On → Pred ( E , On , 𝑏 ) = 𝑏 )
22	21	3ad2ant2	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → Pred ( E , On , 𝑏 ) = 𝑏 )
23		predon	⊢ ( 𝑐 ∈ On → Pred ( E , On , 𝑐 ) = 𝑐 )
24	23	3ad2ant3	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → Pred ( E , On , 𝑐 ) = 𝑐 )
25	24	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜃 ↔ ∀ 𝑓 ∈ 𝑐 𝜃 ) )
26	22 25	raleqbidv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜃 ↔ ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜃 ) )
27	20 26	raleqbidv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜃 ↔ ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜃 ) )
28	22	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) 𝜒 ↔ ∀ 𝑒 ∈ 𝑏 𝜒 ) )
29	20 28	raleqbidv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) 𝜒 ↔ ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 𝜒 ) )
30	24	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜁 ↔ ∀ 𝑓 ∈ 𝑐 𝜁 ) )
31	20 30	raleqbidv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜁 ↔ ∀ 𝑑 ∈ 𝑎 ∀ 𝑓 ∈ 𝑐 𝜁 ) )
32	27 29 31	3anbi123d	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ( ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜁 ) ↔ ( ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜃 ∧ ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 𝜒 ∧ ∀ 𝑑 ∈ 𝑎 ∀ 𝑓 ∈ 𝑐 𝜁 ) ) )
33	20	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) 𝜓 ↔ ∀ 𝑑 ∈ 𝑎 𝜓 ) )
34	24	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜏 ↔ ∀ 𝑓 ∈ 𝑐 𝜏 ) )
35	22 34	raleqbidv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜏 ↔ ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜏 ) )
36	22	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) 𝜎 ↔ ∀ 𝑒 ∈ 𝑏 𝜎 ) )
37	33 35 36	3anbi123d	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ( ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) 𝜎 ) ↔ ( ∀ 𝑑 ∈ 𝑎 𝜓 ∧ ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜏 ∧ ∀ 𝑒 ∈ 𝑏 𝜎 ) ) )
38	24	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜂 ↔ ∀ 𝑓 ∈ 𝑐 𝜂 ) )
39	32 37 38	3anbi123d	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ( ( ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜂 ) ↔ ( ( ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜃 ∧ ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 𝜒 ∧ ∀ 𝑑 ∈ 𝑎 ∀ 𝑓 ∈ 𝑐 𝜁 ) ∧ ( ∀ 𝑑 ∈ 𝑎 𝜓 ∧ ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜏 ∧ ∀ 𝑒 ∈ 𝑏 𝜎 ) ∧ ∀ 𝑓 ∈ 𝑐 𝜂 ) ) )
40	39 11	sylbid	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ( ( ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜂 ) → 𝜑 ) )
41	12 13 17 18 13 17 18 13 17 18 1 2 3 4 5 6 7 8 9 10 40	xpord3ind	⊢ ( ( 𝑋 ∈ On ∧ 𝑌 ∈ On ∧ 𝑍 ∈ On ) → 𝜆 )