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	$⊢ κ \to X \in A$
	xpord3indd.y	$⊢ κ \to Y \in B$
	xpord3indd.z	$⊢ κ \to Z \in C$
	xpord3indd.1	$⊢ κ \to R Fr A$
	xpord3indd.2	$⊢ κ \to R Po A$
	xpord3indd.3	$⊢ κ \to R Se A$
	xpord3indd.4	$⊢ κ \to S Fr B$
	xpord3indd.5	$⊢ κ \to S Po B$
	xpord3indd.6	$⊢ κ \to S Se B$
	xpord3indd.7	$⊢ κ \to T Fr C$
	xpord3indd.8	$⊢ κ \to T Po C$
	xpord3indd.9	$⊢ κ \to T Se C$
	xpord3indd.10	$⊢ a = d \to (φ \leftrightarrow ψ)$
	xpord3indd.11	$⊢ b = e \to (ψ \leftrightarrow χ)$
	xpord3indd.12	$⊢ c = f \to (χ \leftrightarrow θ)$
	xpord3indd.13	$⊢ a = d \to (τ \leftrightarrow θ)$
	xpord3indd.14	$⊢ b = e \to (η \leftrightarrow τ)$
	xpord3indd.15	$⊢ b = e \to (ζ \leftrightarrow θ)$
	xpord3indd.16	$⊢ c = f \to (σ \leftrightarrow τ)$
	xpord3indd.17	$⊢ a = X \to (φ \leftrightarrow ρ)$
	xpord3indd.18	$⊢ b = Y \to (ρ \leftrightarrow μ)$
	xpord3indd.19	$⊢ c = Z \to (μ \leftrightarrow λ)$
	xpord3indd.i	$⊢ (κ \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 φ)$
Assertion	xpord3indd	$⊢ κ \to λ$

Proof

Step	Hyp	Ref	Expression
1		xpord3indd.x	$⊢ κ \to X \in A$
2		xpord3indd.y	$⊢ κ \to Y \in B$
3		xpord3indd.z	$⊢ κ \to Z \in C$
4		xpord3indd.1	$⊢ κ \to R Fr A$
5		xpord3indd.2	$⊢ κ \to R Po A$
6		xpord3indd.3	$⊢ κ \to R Se A$
7		xpord3indd.4	$⊢ κ \to S Fr B$
8		xpord3indd.5	$⊢ κ \to S Po B$
9		xpord3indd.6	$⊢ κ \to S Se B$
10		xpord3indd.7	$⊢ κ \to T Fr C$
11		xpord3indd.8	$⊢ κ \to T Po C$
12		xpord3indd.9	$⊢ κ \to T Se C$
13		xpord3indd.10	$⊢ a = d \to (φ \leftrightarrow ψ)$
14		xpord3indd.11	$⊢ b = e \to (ψ \leftrightarrow χ)$
15		xpord3indd.12	$⊢ c = f \to (χ \leftrightarrow θ)$
16		xpord3indd.13	$⊢ a = d \to (τ \leftrightarrow θ)$
17		xpord3indd.14	$⊢ b = e \to (η \leftrightarrow τ)$
18		xpord3indd.15	$⊢ b = e \to (ζ \leftrightarrow θ)$
19		xpord3indd.16	$⊢ c = f \to (σ \leftrightarrow τ)$
20		xpord3indd.17	$⊢ a = X \to (φ \leftrightarrow ρ)$
21		xpord3indd.18	$⊢ b = Y \to (ρ \leftrightarrow μ)$
22		xpord3indd.19	$⊢ c = Z \to (μ \leftrightarrow λ)$
23		xpord3indd.i	$⊢ (κ \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 φ)$
24		eqid	$⊢ \{⟨x, y⟩ \| (x \in ((A \times B) \times C) \land y \in ((A \times B) \times C) \land (((1^{st} (1^{st} (x)) R 1^{st} (1^{st} (y)) \lor 1^{st} (1^{st} (x)) = 1^{st} (1^{st} (y))) \land (2^{nd} (1^{st} (x)) S 2^{nd} (1^{st} (y)) \lor 2^{nd} (1^{st} (x)) = 2^{nd} (1^{st} (y))) \land (2^{nd} (x) T 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y))) \land x \neq y))\} = \{⟨x, y⟩ \| (x \in ((A \times B) \times C) \land y \in ((A \times B) \times C) \land (((1^{st} (1^{st} (x)) R 1^{st} (1^{st} (y)) \lor 1^{st} (1^{st} (x)) = 1^{st} (1^{st} (y))) \land (2^{nd} (1^{st} (x)) S 2^{nd} (1^{st} (y)) \lor 2^{nd} (1^{st} (x)) = 2^{nd} (1^{st} (y))) \land (2^{nd} (x) T 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y))) \land x \neq y))\}$
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	$⊢ κ \to λ$

Metamath Proof Explorer

Theorem xpord3indd

Proof