Metamath Proof Explorer

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 ⊢ R Fr A
xpord3ind.2 ⊢ R Po A
xpord3ind.3 ⊢ R Se A
xpord3ind.4 ⊢ S Fr B
xpord3ind.5 ⊢ S Po B
xpord3ind.6 ⊢ S Se B
xpord3ind.7 ⊢ T Fr C
xpord3ind.8 ⊢ T Po C
xpord3ind.9 ⊢ T Se C
xpord3ind.10 ⊢ a = d → φ ↔ ψ
xpord3ind.11 ⊢ b = e → ψ ↔ χ
xpord3ind.12 ⊢ c = f → χ ↔ θ
xpord3ind.13 ⊢ a = d → τ ↔ θ
xpord3ind.14 ⊢ b = e → η ↔ τ
xpord3ind.15 ⊢ b = e → ζ ↔ θ
xpord3ind.16 ⊢ c = f → σ ↔ τ
xpord3ind.17 ⊢ a = X → φ ↔ ρ
xpord3ind.18 ⊢ b = Y → ρ ↔ μ
xpord3ind.19 ⊢ c = Z → μ ↔ λ
xpord3ind.i ⊢ a ∈ A ∧ b ∈ B ∧ c ∈ C → ∀ d ∈ Pred R A a ∀ e ∈ Pred S B b ∀ f ∈ Pred T C c θ ∧ ∀ d ∈ Pred R A a ∀ e ∈ Pred S B b χ ∧ ∀ d ∈ Pred R A a ∀ f ∈ Pred T C c ζ ∧ ∀ d ∈ Pred R A a ψ ∧ ∀ e ∈ Pred S B b ∀ f ∈ Pred T C c τ ∧ ∀ e ∈ Pred S B b σ ∧ ∀ f ∈ Pred T C c η → φ
Assertion xpord3ind ⊢ X ∈ A ∧ Y ∈ B ∧ Z ∈ C → λ

Proof

Step Hyp Ref Expression
1 xpord3ind.1 ⊢ R Fr A
2 xpord3ind.2 ⊢ R Po A
3 xpord3ind.3 ⊢ R Se A
4 xpord3ind.4 ⊢ S Fr B
5 xpord3ind.5 ⊢ S Po B
6 xpord3ind.6 ⊢ S Se B
7 xpord3ind.7 ⊢ T Fr C
8 xpord3ind.8 ⊢ T Po C
9 xpord3ind.9 ⊢ T Se C
10 xpord3ind.10 ⊢ a = d → φ ↔ ψ
11 xpord3ind.11 ⊢ b = e → ψ ↔ χ
12 xpord3ind.12 ⊢ c = f → χ ↔ θ
13 xpord3ind.13 ⊢ a = d → τ ↔ θ
14 xpord3ind.14 ⊢ b = e → η ↔ τ
15 xpord3ind.15 ⊢ b = e → ζ ↔ θ
16 xpord3ind.16 ⊢ c = f → σ ↔ τ
17 xpord3ind.17 ⊢ a = X → φ ↔ ρ
18 xpord3ind.18 ⊢ b = Y → ρ ↔ μ
19 xpord3ind.19 ⊢ c = Z → μ ↔ λ
20 xpord3ind.i ⊢ a ∈ A ∧ b ∈ B ∧ c ∈ C → ∀ d ∈ Pred R A a ∀ e ∈ Pred S B b ∀ f ∈ Pred T C c θ ∧ ∀ d ∈ Pred R A a ∀ e ∈ Pred S B b χ ∧ ∀ d ∈ Pred R A a ∀ f ∈ Pred T C c ζ ∧ ∀ d ∈ Pred R A a ψ ∧ ∀ e ∈ Pred S B b ∀ f ∈ Pred T C c τ ∧ ∀ e ∈ Pred S B b σ ∧ ∀ f ∈ Pred T C c η → φ
21 simp1 ⊢ X ∈ A ∧ Y ∈ B ∧ Z ∈ C → X ∈ A
22 simp2 ⊢ X ∈ A ∧ Y ∈ B ∧ Z ∈ C → Y ∈ B
23 simp3 ⊢ X ∈ A ∧ Y ∈ B ∧ Z ∈ C → Z ∈ C
24 ax-1 ⊢ R Fr A → X ∈ A ∧ Y ∈ B ∧ Z ∈ C → R Fr A
25 1 24 ax-mp ⊢ X ∈ A ∧ Y ∈ B ∧ Z ∈ C → R Fr A
26 2 a1i ⊢ X ∈ A ∧ Y ∈ B ∧ Z ∈ C → R Po A
27 3 a1i ⊢ X ∈ A ∧ Y ∈ B ∧ Z ∈ C → R Se A
28 4 a1i ⊢ X ∈ A ∧ Y ∈ B ∧ Z ∈ C → S Fr B
29 5 a1i ⊢ X ∈ A ∧ Y ∈ B ∧ Z ∈ C → S Po B
30 6 a1i ⊢ X ∈ A ∧ Y ∈ B ∧ Z ∈ C → S Se B
31 7 a1i ⊢ X ∈ A ∧ Y ∈ B ∧ Z ∈ C → T Fr C
32 8 a1i ⊢ X ∈ A ∧ Y ∈ B ∧ Z ∈ C → T Po C
33 9 a1i ⊢ X ∈ A ∧ Y ∈ B ∧ Z ∈ C → T Se C
34 20 adantl ⊢ X ∈ A ∧ Y ∈ B ∧ Z ∈ C ∧ a ∈ A ∧ b ∈ B ∧ c ∈ C → ∀ d ∈ Pred R A a ∀ e ∈ Pred S B b ∀ f ∈ Pred T C c θ ∧ ∀ d ∈ Pred R A a ∀ e ∈ Pred S B b χ ∧ ∀ d ∈ Pred R A a ∀ f ∈ Pred T C c ζ ∧ ∀ d ∈ Pred R A a ψ ∧ ∀ e ∈ Pred S B b ∀ f ∈ Pred T C c τ ∧ ∀ e ∈ Pred S B b σ ∧ ∀ f ∈ Pred T C c η → φ
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 ⊢ X ∈ A ∧ Y ∈ B ∧ Z ∈ C → λ