Metamath Proof Explorer

Theorem xpord2ind

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

		Ref	Expression
	Hypotheses	xpord2ind.1	⊢ 𝑅 Fr 𝐴
		xpord2ind.2	⊢ 𝑅 Po 𝐴
		xpord2ind.3	⊢ 𝑅 Se 𝐴
		xpord2ind.4	⊢ 𝑆 Fr 𝐵
		xpord2ind.5	⊢ 𝑆 Po 𝐵
		xpord2ind.6	⊢ 𝑆 Se 𝐵
		xpord2ind.7	⊢ ( 𝑎 = 𝑐 → ( 𝜑 ↔ 𝜓 ) )
		xpord2ind.8	⊢ ( 𝑏 = 𝑑 → ( 𝜓 ↔ 𝜒 ) )
		xpord2ind.9	⊢ ( 𝑎 = 𝑐 → ( 𝜃 ↔ 𝜒 ) )
		xpord2ind.11	⊢ ( 𝑎 = 𝑋 → ( 𝜑 ↔ 𝜏 ) )
		xpord2ind.12	⊢ ( 𝑏 = 𝑌 → ( 𝜏 ↔ 𝜂 ) )
		xpord2ind.i	⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ( ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜃 ) → 𝜑 ) )
	Assertion	xpord2ind	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		xpord2ind.1	⊢ 𝑅 Fr 𝐴
2		xpord2ind.2	⊢ 𝑅 Po 𝐴
3		xpord2ind.3	⊢ 𝑅 Se 𝐴
4		xpord2ind.4	⊢ 𝑆 Fr 𝐵
5		xpord2ind.5	⊢ 𝑆 Po 𝐵
6		xpord2ind.6	⊢ 𝑆 Se 𝐵
7		xpord2ind.7	⊢ ( 𝑎 = 𝑐 → ( 𝜑 ↔ 𝜓 ) )
8		xpord2ind.8	⊢ ( 𝑏 = 𝑑 → ( 𝜓 ↔ 𝜒 ) )
9		xpord2ind.9	⊢ ( 𝑎 = 𝑐 → ( 𝜃 ↔ 𝜒 ) )
10		xpord2ind.11	⊢ ( 𝑎 = 𝑋 → ( 𝜑 ↔ 𝜏 ) )
11		xpord2ind.12	⊢ ( 𝑏 = 𝑌 → ( 𝜏 ↔ 𝜂 ) )
12		xpord2ind.i	⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ( ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜃 ) → 𝜑 ) )
13		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1^st ‘ 𝑥 ) 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) 𝑆 ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1^st ‘ 𝑥 ) 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) 𝑆 ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
14	13 1 2 3 4 5 6 7 8 9 10 11 12	xpord2indlem	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝜂 )