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 \to (φ \leftrightarrow ψ)$
	xpord3ind.11	$⊢ b = e \to (ψ \leftrightarrow χ)$
	xpord3ind.12	$⊢ c = f \to (χ \leftrightarrow θ)$
	xpord3ind.13	$⊢ a = d \to (τ \leftrightarrow θ)$
	xpord3ind.14	$⊢ b = e \to (η \leftrightarrow τ)$
	xpord3ind.15	$⊢ b = e \to (ζ \leftrightarrow θ)$
	xpord3ind.16	$⊢ c = f \to (σ \leftrightarrow τ)$
	xpord3ind.17	$⊢ a = X \to (φ \leftrightarrow ρ)$
	xpord3ind.18	$⊢ b = Y \to (ρ \leftrightarrow μ)$
	xpord3ind.19	$⊢ c = Z \to (μ \leftrightarrow λ)$
	xpord3ind.i	$⊢ (a \in A \land b \in B \land c \in C) \to (((\forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) θ \land \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) χ \land \forall d \in Pred (R, A, a) \forall f \in Pred (T, C, c) ζ) \land (\forall d \in Pred (R, A, a) ψ \land \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) τ \land \forall e \in Pred (S, B, b) σ) \land \forall f \in Pred (T, C, c) η) \to φ)$
Assertion	xpord3ind	$⊢ (X \in A \land Y \in B \land Z \in C) \to λ$

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

Metamath Proof Explorer

Theorem xpord3ind

Proof