xpord3indd

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, 2-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		xpord3indd.x	⊢ ( 𝜅 → 𝑋 ∈ 𝐴 )
2		xpord3indd.y	⊢ ( 𝜅 → 𝑌 ∈ 𝐵 )
3		xpord3indd.z	⊢ ( 𝜅 → 𝑍 ∈ 𝐶 )
4		xpord3indd.1	⊢ ( 𝜅 → 𝑅 Fr 𝐴 )
5		xpord3indd.2	⊢ ( 𝜅 → 𝑅 Po 𝐴 )
6		xpord3indd.3	⊢ ( 𝜅 → 𝑅 Se 𝐴 )
7		xpord3indd.4	⊢ ( 𝜅 → 𝑆 Fr 𝐵 )
8		xpord3indd.5	⊢ ( 𝜅 → 𝑆 Po 𝐵 )
9		xpord3indd.6	⊢ ( 𝜅 → 𝑆 Se 𝐵 )
10		xpord3indd.7	⊢ ( 𝜅 → 𝑇 Fr 𝐶 )
11		xpord3indd.8	⊢ ( 𝜅 → 𝑇 Po 𝐶 )
12		xpord3indd.9	⊢ ( 𝜅 → 𝑇 Se 𝐶 )
13		xpord3indd.10	⊢ ( 𝑎 = 𝑑 → ( 𝜑 ↔ 𝜓 ) )
14		xpord3indd.11	⊢ ( 𝑏 = 𝑒 → ( 𝜓 ↔ 𝜒 ) )
15		xpord3indd.12	⊢ ( 𝑐 = 𝑓 → ( 𝜒 ↔ 𝜃 ) )
16		xpord3indd.13	⊢ ( 𝑎 = 𝑑 → ( 𝜏 ↔ 𝜃 ) )
17		xpord3indd.14	⊢ ( 𝑏 = 𝑒 → ( 𝜂 ↔ 𝜏 ) )
18		xpord3indd.15	⊢ ( 𝑏 = 𝑒 → ( 𝜁 ↔ 𝜃 ) )
19		xpord3indd.16	⊢ ( 𝑐 = 𝑓 → ( 𝜎 ↔ 𝜏 ) )
20		xpord3indd.17	⊢ ( 𝑎 = 𝑋 → ( 𝜑 ↔ 𝜌 ) )
21		xpord3indd.18	⊢ ( 𝑏 = 𝑌 → ( 𝜌 ↔ 𝜇 ) )
22		xpord3indd.19	⊢ ( 𝑐 = 𝑍 → ( 𝜇 ↔ 𝜆 ) )
23		xpord3indd.i	⊢ ( ( 𝜅 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 ) → 𝜑 ) )
24		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ( 2^nd ‘ 𝑥 ) 𝑇 ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ( 2^nd ‘ 𝑥 ) 𝑇 ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
25	24 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23	xpord3inddlem	⊢ ( 𝜅 → 𝜆 )

Metamath Proof Explorer

Theorem xpord3indd

Proof