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 ⊢ R Fr A
xpord2ind.2 ⊢ R Po A
xpord2ind.3 ⊢ R Se A
xpord2ind.4 ⊢ S Fr B
xpord2ind.5 ⊢ S Po B
xpord2ind.6 ⊢ S Se B
xpord2ind.7 ⊢ a = c → φ ↔ ψ
xpord2ind.8 ⊢ b = d → ψ ↔ χ
xpord2ind.9 ⊢ a = c → θ ↔ χ
xpord2ind.11 ⊢ a = X → φ ↔ τ
xpord2ind.12 ⊢ b = Y → τ ↔ η
xpord2ind.i ⊢ a ∈ A ∧ b ∈ B → ∀ c ∈ Pred R A a ∀ d ∈ Pred S B b χ ∧ ∀ c ∈ Pred R A a ψ ∧ ∀ d ∈ Pred S B b θ → φ
Assertion xpord2ind ⊢ X ∈ A ∧ Y ∈ B → η

Proof

Step Hyp Ref Expression
1 xpord2ind.1 ⊢ R Fr A
2 xpord2ind.2 ⊢ R Po A
3 xpord2ind.3 ⊢ R Se A
4 xpord2ind.4 ⊢ S Fr B
5 xpord2ind.5 ⊢ S Po B
6 xpord2ind.6 ⊢ S Se B
7 xpord2ind.7 ⊢ a = c → φ ↔ ψ
8 xpord2ind.8 ⊢ b = d → ψ ↔ χ
9 xpord2ind.9 ⊢ a = c → θ ↔ χ
10 xpord2ind.11 ⊢ a = X → φ ↔ τ
11 xpord2ind.12 ⊢ b = Y → τ ↔ η
12 xpord2ind.i ⊢ a ∈ A ∧ b ∈ B → ∀ c ∈ Pred R A a ∀ d ∈ Pred S B b χ ∧ ∀ c ∈ Pred R A a ψ ∧ ∀ d ∈ Pred S B b θ → φ
13 eqid ⊢ x y | x ∈ A × B ∧ y ∈ A × B ∧ 1 st ⁡ x R 1 st ⁡ y ∨ 1 st ⁡ x = 1 st ⁡ y ∧ 2 nd ⁡ x S 2 nd ⁡ y ∨ 2 nd ⁡ x = 2 nd ⁡ y ∧ x ≠ y = x y | x ∈ A × B ∧ y ∈ A × B ∧ 1 st ⁡ x R 1 st ⁡ y ∨ 1 st ⁡ x = 1 st ⁡ y ∧ 2 nd ⁡ x S 2 nd ⁡ y ∨ 2 nd ⁡ x = 2 nd ⁡ y ∧ x ≠ y
14 13 1 2 3 4 5 6 7 8 9 10 11 12 xpord2indlem ⊢ X ∈ A ∧ Y ∈ B → η