xpord3inddlem

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

Proof

Step	Hyp	Ref	Expression
1		xpord3.1	$⊢ U = \{⟨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))\}$
2		xpord3inddlem.x	$⊢ κ \to X \in A$
3		xpord3inddlem.y	$⊢ κ \to Y \in B$
4		xpord3inddlem.z	$⊢ κ \to Z \in C$
5		xpord3inddlem.1	$⊢ κ \to R Fr A$
6		xpord3inddlem.2	$⊢ κ \to R Po A$
7		xpord3inddlem.3	$⊢ κ \to R Se A$
8		xpord3inddlem.4	$⊢ κ \to S Fr B$
9		xpord3inddlem.5	$⊢ κ \to S Po B$
10		xpord3inddlem.6	$⊢ κ \to S Se B$
11		xpord3inddlem.7	$⊢ κ \to T Fr C$
12		xpord3inddlem.8	$⊢ κ \to T Po C$
13		xpord3inddlem.9	$⊢ κ \to T Se C$
14		xpord3inddlem.10	$⊢ a = d \to (φ \leftrightarrow ψ)$
15		xpord3inddlem.11	$⊢ b = e \to (ψ \leftrightarrow χ)$
16		xpord3inddlem.12	$⊢ c = f \to (χ \leftrightarrow θ)$
17		xpord3inddlem.13	$⊢ a = d \to (τ \leftrightarrow θ)$
18		xpord3inddlem.14	$⊢ b = e \to (η \leftrightarrow τ)$
19		xpord3inddlem.15	$⊢ b = e \to (ζ \leftrightarrow θ)$
20		xpord3inddlem.16	$⊢ c = f \to (σ \leftrightarrow τ)$
21		xpord3inddlem.17	$⊢ a = X \to (φ \leftrightarrow ρ)$
22		xpord3inddlem.18	$⊢ b = Y \to (ρ \leftrightarrow μ)$
23		xpord3inddlem.19	$⊢ c = Z \to (μ \leftrightarrow λ)$
24		xpord3inddlem.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 φ)$
25	1 5 8 11	frxp3	$⊢ κ \to U Fr ((A \times B) \times C)$
26	1 6 9 12	poxp3	$⊢ κ \to U Po ((A \times B) \times C)$
27	1 7 10 13	sexp3	$⊢ κ \to U Se ((A \times B) \times C)$
28		bi2.04	$⊢ (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to (κ \to θ)) \leftrightarrow (κ \to (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ))$
29	28	3albii	$⊢ \forall d \forall e \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to (κ \to θ)) \leftrightarrow \forall d \forall e \forall f (κ \to (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ))$
30		19.21v	$⊢ \forall f (κ \to (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ)) \leftrightarrow (κ \to \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ))$
31	30	2albii	$⊢ \forall d \forall e \forall f (κ \to (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ)) \leftrightarrow \forall d \forall e (κ \to \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ))$
32		19.21v	$⊢ \forall e (κ \to \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ)) \leftrightarrow (κ \to \forall e \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ))$
33	32	albii	$⊢ \forall d \forall e (κ \to \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ)) \leftrightarrow \forall d (κ \to \forall e \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ))$
34		19.21v	$⊢ \forall d (κ \to \forall e \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ)) \leftrightarrow (κ \to \forall d \forall e \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ))$
35	33 34	bitri	$⊢ \forall d \forall e (κ \to \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ)) \leftrightarrow (κ \to \forall d \forall e \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ))$
36	31 35	bitri	$⊢ \forall d \forall e \forall f (κ \to (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ)) \leftrightarrow (κ \to \forall d \forall e \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ))$
37	29 36	bitri	$⊢ \forall d \forall e \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to (κ \to θ)) \leftrightarrow (κ \to \forall d \forall e \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ))$
38	1	xpord3pred	$⊢ (a \in A \land b \in B \land c \in C) \to Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) = (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\}$
39	38	adantl	$⊢ (κ \land (a \in A \land b \in B \land c \in C)) \to Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) = (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\}$
40	39	eleq2d	$⊢ (κ \land (a \in A \land b \in B \land c \in C)) \to (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \leftrightarrow ⟨d, e, f⟩ \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\}))$
41	40	imbi1d	$⊢ (κ \land (a \in A \land b \in B \land c \in C)) \to ((⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ) \leftrightarrow (⟨d, e, f⟩ \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\}) \to θ))$
42		eldifsn	$⊢ ⟨d, e, f⟩ \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\}) \leftrightarrow (⟨d, e, f⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) \land ⟨d, e, f⟩ \neq ⟨a, b, c⟩)$
43		otelxp	$⊢ ⟨d, e, f⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) \leftrightarrow (d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\}) \land f \in (Pred (T, C, c) \cup \{c\}))$
44		vex	$⊢ d \in V$
45		vex	$⊢ e \in V$
46		vex	$⊢ f \in V$
47	44 45 46	otthne	$⊢ ⟨d, e, f⟩ \neq ⟨a, b, c⟩ \leftrightarrow (d \neq a \lor e \neq b \lor f \neq c)$
48	43 47	anbi12i	$⊢ (⟨d, e, f⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) \land ⟨d, e, f⟩ \neq ⟨a, b, c⟩) \leftrightarrow ((d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\}) \land f \in (Pred (T, C, c) \cup \{c\})) \land (d \neq a \lor e \neq b \lor f \neq c))$
49	42 48	bitri	$⊢ ⟨d, e, f⟩ \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\}) \leftrightarrow ((d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\}) \land f \in (Pred (T, C, c) \cup \{c\})) \land (d \neq a \lor e \neq b \lor f \neq c))$
50	49	imbi1i	$⊢ (⟨d, e, f⟩ \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\}) \to θ) \leftrightarrow (((d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\}) \land f \in (Pred (T, C, c) \cup \{c\})) \land (d \neq a \lor e \neq b \lor f \neq c)) \to θ)$
51	41 50	bitrdi	$⊢ (κ \land (a \in A \land b \in B \land c \in C)) \to ((⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ) \leftrightarrow (((d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\}) \land f \in (Pred (T, C, c) \cup \{c\})) \land (d \neq a \lor e \neq b \lor f \neq c)) \to θ))$
52		impexp	$⊢ (((d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\}) \land f \in (Pred (T, C, c) \cup \{c\})) \land (d \neq a \lor e \neq b \lor f \neq c)) \to θ) \leftrightarrow ((d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\}) \land f \in (Pred (T, C, c) \cup \{c\})) \to ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
53	51 52	bitrdi	$⊢ (κ \land (a \in A \land b \in B \land c \in C)) \to ((⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ) \leftrightarrow ((d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\}) \land f \in (Pred (T, C, c) \cup \{c\})) \to ((d \neq a \lor e \neq b \lor f \neq c) \to θ)))$
54	53	albidv	$⊢ (κ \land (a \in A \land b \in B \land c \in C)) \to (\forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ) \leftrightarrow \forall f ((d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\}) \land f \in (Pred (T, C, c) \cup \{c\})) \to ((d \neq a \lor e \neq b \lor f \neq c) \to θ)))$
55	54	2albidv	$⊢ (κ \land (a \in A \land b \in B \land c \in C)) \to (\forall d \forall e \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ) \leftrightarrow \forall d \forall e \forall f ((d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\}) \land f \in (Pred (T, C, c) \cup \{c\})) \to ((d \neq a \lor e \neq b \lor f \neq c) \to θ)))$
56		r3al	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow \forall d \forall e \forall f ((d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\}) \land f \in (Pred (T, C, c) \cup \{c\})) \to ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
57	56	bicomi	$⊢ \forall d \forall e \forall f ((d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\}) \land f \in (Pred (T, C, c) \cup \{c\})) \to ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \leftrightarrow \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
58	55 57	bitrdi	$⊢ (κ \land (a \in A \land b \in B \land c \in C)) \to (\forall d \forall e \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ) \leftrightarrow \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
59		ssun1	$⊢ Pred (T, C, c) \subseteq Pred (T, C, c) \cup \{c\}$
60		ssralv	$⊢ Pred (T, C, c) \subseteq Pred (T, C, c) \cup \{c\} \to (\forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
61	59 60	ax-mp	$⊢ \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
62	61	ralimi	$⊢ \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
63		ssun1	$⊢ Pred (S, B, b) \subseteq Pred (S, B, b) \cup \{b\}$
64		ssralv	$⊢ Pred (S, B, b) \subseteq Pred (S, B, b) \cup \{b\} \to (\forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
65	63 64	ax-mp	$⊢ \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
66	62 65	syl	$⊢ \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
67	66	ralimi	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
68		ssun1	$⊢ Pred (R, A, a) \subseteq Pred (R, A, a) \cup \{a\}$
69		ssralv	$⊢ Pred (R, A, a) \subseteq Pred (R, A, a) \cup \{a\} \to (\forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
70	68 69	ax-mp	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
71	67 70	syl	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
72	71	adantl	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
73		predpoirr	$⊢ T Po C \to \neg c \in Pred (T, C, c)$
74	12 73	syl	$⊢ κ \to \neg c \in Pred (T, C, c)$
75		eleq1	$⊢ f = c \to (f \in Pred (T, C, c) \leftrightarrow c \in Pred (T, C, c))$
76	75	notbid	$⊢ f = c \to (\neg f \in Pred (T, C, c) \leftrightarrow \neg c \in Pred (T, C, c))$
77	74 76	syl5ibrcom	$⊢ κ \to (f = c \to \neg f \in Pred (T, C, c))$
78	77	necon2ad	$⊢ κ \to (f \in Pred (T, C, c) \to f \neq c)$
79	78	imp	$⊢ (κ \land f \in Pred (T, C, c)) \to f \neq c$
80	79	3mix3d	$⊢ (κ \land f \in Pred (T, C, c)) \to (d \neq a \lor e \neq b \lor f \neq c)$
81		pm2.27	$⊢ (d \neq a \lor e \neq b \lor f \neq c) \to (((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to θ)$
82	80 81	syl	$⊢ (κ \land f \in Pred (T, C, c)) \to (((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to θ)$
83	82	ralimdva	$⊢ κ \to (\forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall f \in Pred (T, C, c) θ)$
84	83	ralimdv	$⊢ κ \to (\forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) θ)$
85	84	ralimdv	$⊢ κ \to (\forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) θ)$
86	85	adantr	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to (\forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) θ)$
87	72 86	mpd	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) θ$
88		ssun2	$⊢ \{c\} \subseteq Pred (T, C, c) \cup \{c\}$
89		ssralv	$⊢ \{c\} \subseteq Pred (T, C, c) \cup \{c\} \to (\forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
90	88 89	ax-mp	$⊢ \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
91	90	ralimi	$⊢ \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
92		ssralv	$⊢ Pred (S, B, b) \subseteq Pred (S, B, b) \cup \{b\} \to (\forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
93	63 92	ax-mp	$⊢ \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
94	91 93	syl	$⊢ \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
95	94	ralimi	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
96		ssralv	$⊢ Pred (R, A, a) \subseteq Pred (R, A, a) \cup \{a\} \to (\forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
97	68 96	ax-mp	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
98	95 97	syl	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
99		vex	$⊢ c \in V$
100		biidd	$⊢ f = c \to (d \neq a \leftrightarrow d \neq a)$
101		biidd	$⊢ f = c \to (e \neq b \leftrightarrow e \neq b)$
102		neeq1	$⊢ f = c \to (f \neq c \leftrightarrow c \neq c)$
103	100 101 102	3orbi123d	$⊢ f = c \to ((d \neq a \lor e \neq b \lor f \neq c) \leftrightarrow (d \neq a \lor e \neq b \lor c \neq c))$
104	16	equcoms	$⊢ f = c \to (χ \leftrightarrow θ)$
105	104	bicomd	$⊢ f = c \to (θ \leftrightarrow χ)$
106	103 105	imbi12d	$⊢ f = c \to (((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow ((d \neq a \lor e \neq b \lor c \neq c) \to χ))$
107	99 106	ralsn	$⊢ \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow ((d \neq a \lor e \neq b \lor c \neq c) \to χ)$
108	107	2ralbii	$⊢ \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) ((d \neq a \lor e \neq b \lor c \neq c) \to χ)$
109	98 108	sylib	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) ((d \neq a \lor e \neq b \lor c \neq c) \to χ)$
110	109	adantl	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) ((d \neq a \lor e \neq b \lor c \neq c) \to χ)$
111		predpoirr	$⊢ S Po B \to \neg b \in Pred (S, B, b)$
112	9 111	syl	$⊢ κ \to \neg b \in Pred (S, B, b)$
113		eleq1	$⊢ e = b \to (e \in Pred (S, B, b) \leftrightarrow b \in Pred (S, B, b))$
114	113	notbid	$⊢ e = b \to (\neg e \in Pred (S, B, b) \leftrightarrow \neg b \in Pred (S, B, b))$
115	112 114	syl5ibrcom	$⊢ κ \to (e = b \to \neg e \in Pred (S, B, b))$
116	115	necon2ad	$⊢ κ \to (e \in Pred (S, B, b) \to e \neq b)$
117	116	imp	$⊢ (κ \land e \in Pred (S, B, b)) \to e \neq b$
118	117	3mix2d	$⊢ (κ \land e \in Pred (S, B, b)) \to (d \neq a \lor e \neq b \lor c \neq c)$
119		pm2.27	$⊢ (d \neq a \lor e \neq b \lor c \neq c) \to (((d \neq a \lor e \neq b \lor c \neq c) \to χ) \to χ)$
120	118 119	syl	$⊢ (κ \land e \in Pred (S, B, b)) \to (((d \neq a \lor e \neq b \lor c \neq c) \to χ) \to χ)$
121	120	ralimdva	$⊢ κ \to (\forall e \in Pred (S, B, b) ((d \neq a \lor e \neq b \lor c \neq c) \to χ) \to \forall e \in Pred (S, B, b) χ)$
122	121	ralimdv	$⊢ κ \to (\forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) ((d \neq a \lor e \neq b \lor c \neq c) \to χ) \to \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) χ)$
123	122	adantr	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to (\forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) ((d \neq a \lor e \neq b \lor c \neq c) \to χ) \to \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) χ)$
124	110 123	mpd	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to \forall d \in Pred (R, A, a) \forall e \in Pred (S, B, b) χ$
125		ssun2	$⊢ \{b\} \subseteq Pred (S, B, b) \cup \{b\}$
126		ssralv	$⊢ \{b\} \subseteq Pred (S, B, b) \cup \{b\} \to (\forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
127	125 126	ax-mp	$⊢ \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
128	62 127	syl	$⊢ \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
129	128	ralimi	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
130		ssralv	$⊢ Pred (R, A, a) \subseteq Pred (R, A, a) \cup \{a\} \to (\forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
131	68 130	ax-mp	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
132	129 131	syl	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
133		vex	$⊢ b \in V$
134		biidd	$⊢ e = b \to (d \neq a \leftrightarrow d \neq a)$
135		neeq1	$⊢ e = b \to (e \neq b \leftrightarrow b \neq b)$
136		biidd	$⊢ e = b \to (f \neq c \leftrightarrow f \neq c)$
137	134 135 136	3orbi123d	$⊢ e = b \to ((d \neq a \lor e \neq b \lor f \neq c) \leftrightarrow (d \neq a \lor b \neq b \lor f \neq c))$
138	19	equcoms	$⊢ e = b \to (ζ \leftrightarrow θ)$
139	138	bicomd	$⊢ e = b \to (θ \leftrightarrow ζ)$
140	137 139	imbi12d	$⊢ e = b \to (((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow ((d \neq a \lor b \neq b \lor f \neq c) \to ζ))$
141	140	ralbidv	$⊢ e = b \to (\forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow \forall f \in Pred (T, C, c) ((d \neq a \lor b \neq b \lor f \neq c) \to ζ))$
142	133 141	ralsn	$⊢ \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow \forall f \in Pred (T, C, c) ((d \neq a \lor b \neq b \lor f \neq c) \to ζ)$
143	142	ralbii	$⊢ \forall d \in Pred (R, A, a) \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow \forall d \in Pred (R, A, a) \forall f \in Pred (T, C, c) ((d \neq a \lor b \neq b \lor f \neq c) \to ζ)$
144	132 143	sylib	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall f \in Pred (T, C, c) ((d \neq a \lor b \neq b \lor f \neq c) \to ζ)$
145	144	adantl	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to \forall d \in Pred (R, A, a) \forall f \in Pred (T, C, c) ((d \neq a \lor b \neq b \lor f \neq c) \to ζ)$
146	79	3mix3d	$⊢ (κ \land f \in Pred (T, C, c)) \to (d \neq a \lor b \neq b \lor f \neq c)$
147		pm2.27	$⊢ (d \neq a \lor b \neq b \lor f \neq c) \to (((d \neq a \lor b \neq b \lor f \neq c) \to ζ) \to ζ)$
148	146 147	syl	$⊢ (κ \land f \in Pred (T, C, c)) \to (((d \neq a \lor b \neq b \lor f \neq c) \to ζ) \to ζ)$
149	148	ralimdva	$⊢ κ \to (\forall f \in Pred (T, C, c) ((d \neq a \lor b \neq b \lor f \neq c) \to ζ) \to \forall f \in Pred (T, C, c) ζ)$
150	149	ralimdv	$⊢ κ \to (\forall d \in Pred (R, A, a) \forall f \in Pred (T, C, c) ((d \neq a \lor b \neq b \lor f \neq c) \to ζ) \to \forall d \in Pred (R, A, a) \forall f \in Pred (T, C, c) ζ)$
151	150	adantr	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to (\forall d \in Pred (R, A, a) \forall f \in Pred (T, C, c) ((d \neq a \lor b \neq b \lor f \neq c) \to ζ) \to \forall d \in Pred (R, A, a) \forall f \in Pred (T, C, c) ζ)$
152	145 151	mpd	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to \forall d \in Pred (R, A, a) \forall f \in Pred (T, C, c) ζ$
153	87 124 152	3jca	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \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) ζ)$
154		ssralv	$⊢ \{b\} \subseteq Pred (S, B, b) \cup \{b\} \to (\forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in \{b\} \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
155	125 154	ax-mp	$⊢ \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in \{b\} \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
156	91 155	syl	$⊢ \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in \{b\} \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
157	156	ralimi	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in \{b\} \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
158		ssralv	$⊢ Pred (R, A, a) \subseteq Pred (R, A, a) \cup \{a\} \to (\forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in \{b\} \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall e \in \{b\} \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
159	68 158	ax-mp	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in \{b\} \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall e \in \{b\} \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
160	157 159	syl	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) \forall e \in \{b\} \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
161	107	ralbii	$⊢ \forall e \in \{b\} \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow \forall e \in \{b\} ((d \neq a \lor e \neq b \lor c \neq c) \to χ)$
162		biidd	$⊢ e = b \to (c \neq c \leftrightarrow c \neq c)$
163	134 135 162	3orbi123d	$⊢ e = b \to ((d \neq a \lor e \neq b \lor c \neq c) \leftrightarrow (d \neq a \lor b \neq b \lor c \neq c))$
164	15	equcoms	$⊢ e = b \to (ψ \leftrightarrow χ)$
165	164	bicomd	$⊢ e = b \to (χ \leftrightarrow ψ)$
166	163 165	imbi12d	$⊢ e = b \to (((d \neq a \lor e \neq b \lor c \neq c) \to χ) \leftrightarrow ((d \neq a \lor b \neq b \lor c \neq c) \to ψ))$
167	133 166	ralsn	$⊢ \forall e \in \{b\} ((d \neq a \lor e \neq b \lor c \neq c) \to χ) \leftrightarrow ((d \neq a \lor b \neq b \lor c \neq c) \to ψ)$
168	161 167	bitri	$⊢ \forall e \in \{b\} \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow ((d \neq a \lor b \neq b \lor c \neq c) \to ψ)$
169	168	ralbii	$⊢ \forall d \in Pred (R, A, a) \forall e \in \{b\} \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow \forall d \in Pred (R, A, a) ((d \neq a \lor b \neq b \lor c \neq c) \to ψ)$
170	160 169	sylib	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in Pred (R, A, a) ((d \neq a \lor b \neq b \lor c \neq c) \to ψ)$
171	170	adantl	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to \forall d \in Pred (R, A, a) ((d \neq a \lor b \neq b \lor c \neq c) \to ψ)$
172		predpoirr	$⊢ R Po A \to \neg a \in Pred (R, A, a)$
173	6 172	syl	$⊢ κ \to \neg a \in Pred (R, A, a)$
174		eleq1	$⊢ d = a \to (d \in Pred (R, A, a) \leftrightarrow a \in Pred (R, A, a))$
175	174	notbid	$⊢ d = a \to (\neg d \in Pred (R, A, a) \leftrightarrow \neg a \in Pred (R, A, a))$
176	173 175	syl5ibrcom	$⊢ κ \to (d = a \to \neg d \in Pred (R, A, a))$
177	176	necon2ad	$⊢ κ \to (d \in Pred (R, A, a) \to d \neq a)$
178	177	imp	$⊢ (κ \land d \in Pred (R, A, a)) \to d \neq a$
179	178	3mix1d	$⊢ (κ \land d \in Pred (R, A, a)) \to (d \neq a \lor b \neq b \lor c \neq c)$
180		pm2.27	$⊢ (d \neq a \lor b \neq b \lor c \neq c) \to (((d \neq a \lor b \neq b \lor c \neq c) \to ψ) \to ψ)$
181	179 180	syl	$⊢ (κ \land d \in Pred (R, A, a)) \to (((d \neq a \lor b \neq b \lor c \neq c) \to ψ) \to ψ)$
182	181	ralimdva	$⊢ κ \to (\forall d \in Pred (R, A, a) ((d \neq a \lor b \neq b \lor c \neq c) \to ψ) \to \forall d \in Pred (R, A, a) ψ)$
183	182	adantr	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to (\forall d \in Pred (R, A, a) ((d \neq a \lor b \neq b \lor c \neq c) \to ψ) \to \forall d \in Pred (R, A, a) ψ)$
184	171 183	mpd	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to \forall d \in Pred (R, A, a) ψ$
185		ssun2	$⊢ \{a\} \subseteq Pred (R, A, a) \cup \{a\}$
186		ssralv	$⊢ \{a\} \subseteq Pred (R, A, a) \cup \{a\} \to (\forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in \{a\} \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
187	185 186	ax-mp	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in \{a\} \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
188	67 187	syl	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in \{a\} \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
189		vex	$⊢ a \in V$
190		neeq1	$⊢ d = a \to (d \neq a \leftrightarrow a \neq a)$
191		biidd	$⊢ d = a \to (e \neq b \leftrightarrow e \neq b)$
192		biidd	$⊢ d = a \to (f \neq c \leftrightarrow f \neq c)$
193	190 191 192	3orbi123d	$⊢ d = a \to ((d \neq a \lor e \neq b \lor f \neq c) \leftrightarrow (a \neq a \lor e \neq b \lor f \neq c))$
194	17	equcoms	$⊢ d = a \to (τ \leftrightarrow θ)$
195	194	bicomd	$⊢ d = a \to (θ \leftrightarrow τ)$
196	193 195	imbi12d	$⊢ d = a \to (((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow ((a \neq a \lor e \neq b \lor f \neq c) \to τ))$
197	196	2ralbidv	$⊢ d = a \to (\forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((a \neq a \lor e \neq b \lor f \neq c) \to τ))$
198	189 197	ralsn	$⊢ \forall d \in \{a\} \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((a \neq a \lor e \neq b \lor f \neq c) \to τ)$
199	188 198	sylib	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((a \neq a \lor e \neq b \lor f \neq c) \to τ)$
200	199	adantl	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((a \neq a \lor e \neq b \lor f \neq c) \to τ)$
201	79	3mix3d	$⊢ (κ \land f \in Pred (T, C, c)) \to (a \neq a \lor e \neq b \lor f \neq c)$
202		pm2.27	$⊢ (a \neq a \lor e \neq b \lor f \neq c) \to (((a \neq a \lor e \neq b \lor f \neq c) \to τ) \to τ)$
203	201 202	syl	$⊢ (κ \land f \in Pred (T, C, c)) \to (((a \neq a \lor e \neq b \lor f \neq c) \to τ) \to τ)$
204	203	ralimdva	$⊢ κ \to (\forall f \in Pred (T, C, c) ((a \neq a \lor e \neq b \lor f \neq c) \to τ) \to \forall f \in Pred (T, C, c) τ)$
205	204	ralimdv	$⊢ κ \to (\forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((a \neq a \lor e \neq b \lor f \neq c) \to τ) \to \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) τ)$
206	205	adantr	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to (\forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) ((a \neq a \lor e \neq b \lor f \neq c) \to τ) \to \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) τ)$
207	200 206	mpd	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to \forall e \in Pred (S, B, b) \forall f \in Pred (T, C, c) τ$
208		ssralv	$⊢ \{a\} \subseteq Pred (R, A, a) \cup \{a\} \to (\forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in \{a\} \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
209	185 208	ax-mp	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in \{a\} \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
210	95 209	syl	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in \{a\} \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
211	196	2ralbidv	$⊢ d = a \to (\forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow \forall e \in Pred (S, B, b) \forall f \in \{c\} ((a \neq a \lor e \neq b \lor f \neq c) \to τ))$
212	189 211	ralsn	$⊢ \forall d \in \{a\} \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow \forall e \in Pred (S, B, b) \forall f \in \{c\} ((a \neq a \lor e \neq b \lor f \neq c) \to τ)$
213		biidd	$⊢ f = c \to (a \neq a \leftrightarrow a \neq a)$
214	213 101 102	3orbi123d	$⊢ f = c \to ((a \neq a \lor e \neq b \lor f \neq c) \leftrightarrow (a \neq a \lor e \neq b \lor c \neq c))$
215	20	bicomd	$⊢ c = f \to (τ \leftrightarrow σ)$
216	215	equcoms	$⊢ f = c \to (τ \leftrightarrow σ)$
217	214 216	imbi12d	$⊢ f = c \to (((a \neq a \lor e \neq b \lor f \neq c) \to τ) \leftrightarrow ((a \neq a \lor e \neq b \lor c \neq c) \to σ))$
218	99 217	ralsn	$⊢ \forall f \in \{c\} ((a \neq a \lor e \neq b \lor f \neq c) \to τ) \leftrightarrow ((a \neq a \lor e \neq b \lor c \neq c) \to σ)$
219	218	ralbii	$⊢ \forall e \in Pred (S, B, b) \forall f \in \{c\} ((a \neq a \lor e \neq b \lor f \neq c) \to τ) \leftrightarrow \forall e \in Pred (S, B, b) ((a \neq a \lor e \neq b \lor c \neq c) \to σ)$
220	212 219	bitri	$⊢ \forall d \in \{a\} \forall e \in Pred (S, B, b) \forall f \in \{c\} ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow \forall e \in Pred (S, B, b) ((a \neq a \lor e \neq b \lor c \neq c) \to σ)$
221	210 220	sylib	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall e \in Pred (S, B, b) ((a \neq a \lor e \neq b \lor c \neq c) \to σ)$
222	221	adantl	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to \forall e \in Pred (S, B, b) ((a \neq a \lor e \neq b \lor c \neq c) \to σ)$
223	117	3mix2d	$⊢ (κ \land e \in Pred (S, B, b)) \to (a \neq a \lor e \neq b \lor c \neq c)$
224		pm2.27	$⊢ (a \neq a \lor e \neq b \lor c \neq c) \to (((a \neq a \lor e \neq b \lor c \neq c) \to σ) \to σ)$
225	223 224	syl	$⊢ (κ \land e \in Pred (S, B, b)) \to (((a \neq a \lor e \neq b \lor c \neq c) \to σ) \to σ)$
226	225	ralimdva	$⊢ κ \to (\forall e \in Pred (S, B, b) ((a \neq a \lor e \neq b \lor c \neq c) \to σ) \to \forall e \in Pred (S, B, b) σ)$
227	226	adantr	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to (\forall e \in Pred (S, B, b) ((a \neq a \lor e \neq b \lor c \neq c) \to σ) \to \forall e \in Pred (S, B, b) σ)$
228	222 227	mpd	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to \forall e \in Pred (S, B, b) σ$
229	184 207 228	3jca	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to (\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) σ)$
230		ssralv	$⊢ \{a\} \subseteq Pred (R, A, a) \cup \{a\} \to (\forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in \{a\} \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
231	185 230	ax-mp	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in \{a\} \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
232	129 231	syl	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall d \in \{a\} \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
233	196	2ralbidv	$⊢ d = a \to (\forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow \forall e \in \{b\} \forall f \in Pred (T, C, c) ((a \neq a \lor e \neq b \lor f \neq c) \to τ))$
234	189 233	ralsn	$⊢ \forall d \in \{a\} \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow \forall e \in \{b\} \forall f \in Pred (T, C, c) ((a \neq a \lor e \neq b \lor f \neq c) \to τ)$
235		biidd	$⊢ e = b \to (a \neq a \leftrightarrow a \neq a)$
236	235 135 136	3orbi123d	$⊢ e = b \to ((a \neq a \lor e \neq b \lor f \neq c) \leftrightarrow (a \neq a \lor b \neq b \lor f \neq c))$
237		equcomi	$⊢ e = b \to b = e$
238		bicom1	$⊢ (η \leftrightarrow τ) \to (τ \leftrightarrow η)$
239	237 18 238	3syl	$⊢ e = b \to (τ \leftrightarrow η)$
240	236 239	imbi12d	$⊢ e = b \to (((a \neq a \lor e \neq b \lor f \neq c) \to τ) \leftrightarrow ((a \neq a \lor b \neq b \lor f \neq c) \to η))$
241	240	ralbidv	$⊢ e = b \to (\forall f \in Pred (T, C, c) ((a \neq a \lor e \neq b \lor f \neq c) \to τ) \leftrightarrow \forall f \in Pred (T, C, c) ((a \neq a \lor b \neq b \lor f \neq c) \to η))$
242	133 241	ralsn	$⊢ \forall e \in \{b\} \forall f \in Pred (T, C, c) ((a \neq a \lor e \neq b \lor f \neq c) \to τ) \leftrightarrow \forall f \in Pred (T, C, c) ((a \neq a \lor b \neq b \lor f \neq c) \to η)$
243	234 242	bitri	$⊢ \forall d \in \{a\} \forall e \in \{b\} \forall f \in Pred (T, C, c) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \leftrightarrow \forall f \in Pred (T, C, c) ((a \neq a \lor b \neq b \lor f \neq c) \to η)$
244	232 243	sylib	$⊢ \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to \forall f \in Pred (T, C, c) ((a \neq a \lor b \neq b \lor f \neq c) \to η)$
245	244	adantl	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to \forall f \in Pred (T, C, c) ((a \neq a \lor b \neq b \lor f \neq c) \to η)$
246	79	3mix3d	$⊢ (κ \land f \in Pred (T, C, c)) \to (a \neq a \lor b \neq b \lor f \neq c)$
247		pm2.27	$⊢ (a \neq a \lor b \neq b \lor f \neq c) \to (((a \neq a \lor b \neq b \lor f \neq c) \to η) \to η)$
248	246 247	syl	$⊢ (κ \land f \in Pred (T, C, c)) \to (((a \neq a \lor b \neq b \lor f \neq c) \to η) \to η)$
249	248	ralimdva	$⊢ κ \to (\forall f \in Pred (T, C, c) ((a \neq a \lor b \neq b \lor f \neq c) \to η) \to \forall f \in Pred (T, C, c) η)$
250	249	adantr	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to (\forall f \in Pred (T, C, c) ((a \neq a \lor b \neq b \lor f \neq c) \to η) \to \forall f \in Pred (T, C, c) η)$
251	245 250	mpd	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \to \forall f \in Pred (T, C, c) η$
252	153 229 251	3jca	$⊢ (κ \land \forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)) \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) η)$
253	252	ex	$⊢ κ \to (\forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \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) η))$
254	253	adantr	$⊢ (κ \land (a \in A \land b \in B \land c \in C)) \to (\forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \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) η))$
255	254 24	syld	$⊢ (κ \land (a \in A \land b \in B \land c \in C)) \to (\forall d \in (Pred (R, A, a) \cup \{a\}) \forall e \in (Pred (S, B, b) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to φ)$
256	58 255	sylbid	$⊢ (κ \land (a \in A \land b \in B \land c \in C)) \to (\forall d \forall e \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ) \to φ)$
257	256	expcom	$⊢ (a \in A \land b \in B \land c \in C) \to (κ \to (\forall d \forall e \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ) \to φ))$
258	257	a2d	$⊢ (a \in A \land b \in B \land c \in C) \to ((κ \to \forall d \forall e \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to θ)) \to (κ \to φ))$
259	37 258	biimtrid	$⊢ (a \in A \land b \in B \land c \in C) \to (\forall d \forall e \forall f (⟨d, e, f⟩ \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \to (κ \to θ)) \to (κ \to φ))$
260	14	imbi2d	$⊢ a = d \to ((κ \to φ) \leftrightarrow (κ \to ψ))$
261	15	imbi2d	$⊢ b = e \to ((κ \to ψ) \leftrightarrow (κ \to χ))$
262	16	imbi2d	$⊢ c = f \to ((κ \to χ) \leftrightarrow (κ \to θ))$
263	21	imbi2d	$⊢ a = X \to ((κ \to φ) \leftrightarrow (κ \to ρ))$
264	22	imbi2d	$⊢ b = Y \to ((κ \to ρ) \leftrightarrow (κ \to μ))$
265	23	imbi2d	$⊢ c = Z \to ((κ \to μ) \leftrightarrow (κ \to λ))$
266	259 260 261 262 263 264 265	frpoins3xp3g	$⊢ ((U Fr ((A \times B) \times C) \land U Po ((A \times B) \times C) \land U Se ((A \times B) \times C)) \land (X \in A \land Y \in B \land Z \in C)) \to (κ \to λ)$
267	25 26 27 2 3 4 266	syl33anc	$⊢ κ \to (κ \to λ)$
268	267	pm2.43i	$⊢ κ \to λ$

Metamath Proof Explorer

Theorem xpord3inddlem

Proof