Theorem xpord3ind

Description: Induction over the triple Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 4-Sep-2024)

	Ref	Expression
Hypotheses	xpord3ind.1	⊢ 𝑅 Fr 𝐴
	xpord3ind.2	⊢ 𝑅 Po 𝐴
	xpord3ind.3	⊢ 𝑅 Se 𝐴
	xpord3ind.4	⊢ 𝑆 Fr 𝐵
	xpord3ind.5	⊢ 𝑆 Po 𝐵
	xpord3ind.6	⊢ 𝑆 Se 𝐵
	xpord3ind.7	⊢ 𝑇 Fr 𝐶
	xpord3ind.8	⊢ 𝑇 Po 𝐶
	xpord3ind.9	⊢ 𝑇 Se 𝐶
	xpord3ind.10	⊢ ( 𝑎 = 𝑑 → ( 𝜑 ↔ 𝜓 ) )
	xpord3ind.11	⊢ ( 𝑏 = 𝑒 → ( 𝜓 ↔ 𝜒 ) )
	xpord3ind.12	⊢ ( 𝑐 = 𝑓 → ( 𝜒 ↔ 𝜃 ) )
	xpord3ind.13	⊢ ( 𝑎 = 𝑑 → ( 𝜏 ↔ 𝜃 ) )
	xpord3ind.14	⊢ ( 𝑏 = 𝑒 → ( 𝜂 ↔ 𝜏 ) )
	xpord3ind.15	⊢ ( 𝑏 = 𝑒 → ( 𝜁 ↔ 𝜃 ) )
	xpord3ind.16	⊢ ( 𝑐 = 𝑓 → ( 𝜎 ↔ 𝜏 ) )
	xpord3ind.17	⊢ ( 𝑎 = 𝑋 → ( 𝜑 ↔ 𝜌 ) )
	xpord3ind.18	⊢ ( 𝑏 = 𝑌 → ( 𝜌 ↔ 𝜇 ) )
	xpord3ind.19	⊢ ( 𝑐 = 𝑍 → ( 𝜇 ↔ 𝜆 ) )
	xpord3ind.i	⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 ) → 𝜑 ) )
Assertion	xpord3ind	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝜆 )

Proof

Step	Hyp	Ref	Expression
1		xpord3ind.1	⊢ 𝑅 Fr 𝐴
2		xpord3ind.2	⊢ 𝑅 Po 𝐴
3		xpord3ind.3	⊢ 𝑅 Se 𝐴
4		xpord3ind.4	⊢ 𝑆 Fr 𝐵
5		xpord3ind.5	⊢ 𝑆 Po 𝐵
6		xpord3ind.6	⊢ 𝑆 Se 𝐵
7		xpord3ind.7	⊢ 𝑇 Fr 𝐶
8		xpord3ind.8	⊢ 𝑇 Po 𝐶
9		xpord3ind.9	⊢ 𝑇 Se 𝐶
10		xpord3ind.10	⊢ ( 𝑎 = 𝑑 → ( 𝜑 ↔ 𝜓 ) )
11		xpord3ind.11	⊢ ( 𝑏 = 𝑒 → ( 𝜓 ↔ 𝜒 ) )
12		xpord3ind.12	⊢ ( 𝑐 = 𝑓 → ( 𝜒 ↔ 𝜃 ) )
13		xpord3ind.13	⊢ ( 𝑎 = 𝑑 → ( 𝜏 ↔ 𝜃 ) )
14		xpord3ind.14	⊢ ( 𝑏 = 𝑒 → ( 𝜂 ↔ 𝜏 ) )
15		xpord3ind.15	⊢ ( 𝑏 = 𝑒 → ( 𝜁 ↔ 𝜃 ) )
16		xpord3ind.16	⊢ ( 𝑐 = 𝑓 → ( 𝜎 ↔ 𝜏 ) )
17		xpord3ind.17	⊢ ( 𝑎 = 𝑋 → ( 𝜑 ↔ 𝜌 ) )
18		xpord3ind.18	⊢ ( 𝑏 = 𝑌 → ( 𝜌 ↔ 𝜇 ) )
19		xpord3ind.19	⊢ ( 𝑐 = 𝑍 → ( 𝜇 ↔ 𝜆 ) )
20		xpord3ind.i	⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 ) → 𝜑 ) )
21		simp1	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝑋 ∈ 𝐴 )
22		simp2	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝑌 ∈ 𝐵 )
23		simp3	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝑍 ∈ 𝐶 )
24		ax-1	⊢ ( 𝑅 Fr 𝐴 → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝑅 Fr 𝐴 ) )
25	1 24	ax-mp	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝑅 Fr 𝐴 )
26	2	a1i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝑅 Po 𝐴 )
27	3	a1i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝑅 Se 𝐴 )
28	4	a1i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝑆 Fr 𝐵 )
29	5	a1i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝑆 Po 𝐵 )
30	6	a1i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝑆 Se 𝐵 )
31	7	a1i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝑇 Fr 𝐶 )
32	8	a1i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝑇 Po 𝐶 )
33	9	a1i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝑇 Se 𝐶 )
34	20	adantl	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 ) → 𝜑 ) )
35	21 22 23 25 26 27 28 29 30 31 32 33 10 11 12 13 14 15 16 17 18 19 34	xpord3indd	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝜆 )