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		onfr	⊢ E Fr On
13		epweon	⊢ E We On
14		weso	⊢ ( E We On → E Or On )
15		sopo	⊢ ( E Or On → E Po On )
16	13 14 15	mp2b	⊢ E Po On
17		epse	⊢ E Se On
18		predon	⊢ ( 𝑎 ∈ On → Pred ( E , On , 𝑎 ) = 𝑎 )
19	18	3ad2ant1	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → Pred ( E , On , 𝑎 ) = 𝑎 )
20		predon	⊢ ( 𝑏 ∈ On → Pred ( E , On , 𝑏 ) = 𝑏 )
21	20	3ad2ant2	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → Pred ( E , On , 𝑏 ) = 𝑏 )
22		predon	⊢ ( 𝑐 ∈ On → Pred ( E , On , 𝑐 ) = 𝑐 )
23	22	3ad2ant3	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → Pred ( E , On , 𝑐 ) = 𝑐 )
24	23	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜃 ↔ ∀ 𝑓 ∈ 𝑐 𝜃 ) )
25	21 24	raleqbidv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜃 ↔ ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜃 ) )
26	19 25	raleqbidv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜃 ↔ ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜃 ) )
27	21	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) 𝜒 ↔ ∀ 𝑒 ∈ 𝑏 𝜒 ) )
28	19 27	raleqbidv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) 𝜒 ↔ ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 𝜒 ) )
29	23	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜁 ↔ ∀ 𝑓 ∈ 𝑐 𝜁 ) )
30	19 29	raleqbidv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜁 ↔ ∀ 𝑑 ∈ 𝑎 ∀ 𝑓 ∈ 𝑐 𝜁 ) )
31	26 28 30	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 , 𝑐 ) 𝜁 ) ↔ ( ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜃 ∧ ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 𝜒 ∧ ∀ 𝑑 ∈ 𝑎 ∀ 𝑓 ∈ 𝑐 𝜁 ) ) )
32	19	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) 𝜓 ↔ ∀ 𝑑 ∈ 𝑎 𝜓 ) )
33	23	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜏 ↔ ∀ 𝑓 ∈ 𝑐 𝜏 ) )
34	21 33	raleqbidv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜏 ↔ ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜏 ) )
35	21	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) 𝜎 ↔ ∀ 𝑒 ∈ 𝑏 𝜎 ) )
36	32 34 35	3anbi123d	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ( ∀ 𝑑 ∈ Pred ( E , On , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( E , On , 𝑏 ) 𝜎 ) ↔ ( ∀ 𝑑 ∈ 𝑎 𝜓 ∧ ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜏 ∧ ∀ 𝑒 ∈ 𝑏 𝜎 ) ) )
37	23	raleqdv	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ∀ 𝑓 ∈ Pred ( E , On , 𝑐 ) 𝜂 ↔ ∀ 𝑓 ∈ 𝑐 𝜂 ) )
38	31 36 37	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 , 𝑐 ) 𝜂 ) ↔ ( ( ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜃 ∧ ∀ 𝑑 ∈ 𝑎 ∀ 𝑒 ∈ 𝑏 𝜒 ∧ ∀ 𝑑 ∈ 𝑎 ∀ 𝑓 ∈ 𝑐 𝜁 ) ∧ ( ∀ 𝑑 ∈ 𝑎 𝜓 ∧ ∀ 𝑒 ∈ 𝑏 ∀ 𝑓 ∈ 𝑐 𝜏 ∧ ∀ 𝑒 ∈ 𝑏 𝜎 ) ∧ ∀ 𝑓 ∈ 𝑐 𝜂 ) ) )
39	38 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 , 𝑐 ) 𝜂 ) → 𝜑 ) )
40	12 16 17 12 16 17 12 16 17 1 2 3 4 5 6 7 8 9 10 39	xpord3ind	⊢ ( ( 𝑋 ∈ On ∧ 𝑌 ∈ On ∧ 𝑍 ∈ On ) → 𝜆 )