xpord3ind

Description: Induction over the triple cross 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	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))\}$
	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		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		xpord3ind.1	$⊢ R Fr A$
3		xpord3ind.2	$⊢ R Po A$
4		xpord3ind.3	$⊢ R Se A$
5		xpord3ind.4	$⊢ S Fr B$
6		xpord3ind.5	$⊢ S Po B$
7		xpord3ind.6	$⊢ S Se B$
8		xpord3ind.7	$⊢ T Fr C$
9		xpord3ind.8	$⊢ T Po C$
10		xpord3ind.9	$⊢ T Se C$
11		xpord3ind.10	$⊢ a = d \to (φ \leftrightarrow ψ)$
12		xpord3ind.11	$⊢ b = e \to (ψ \leftrightarrow χ)$
13		xpord3ind.12	$⊢ c = f \to (χ \leftrightarrow θ)$
14		xpord3ind.13	$⊢ a = d \to (τ \leftrightarrow θ)$
15		xpord3ind.14	$⊢ b = e \to (η \leftrightarrow τ)$
16		xpord3ind.15	$⊢ b = e \to (ζ \leftrightarrow θ)$
17		xpord3ind.16	$⊢ c = f \to (σ \leftrightarrow τ)$
18		xpord3ind.17	$⊢ a = X \to (φ \leftrightarrow ρ)$
19		xpord3ind.18	$⊢ b = Y \to (ρ \leftrightarrow μ)$
20		xpord3ind.19	$⊢ c = Z \to (μ \leftrightarrow λ)$
21		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 φ)$
22	2	a1i	$⊢ ⊤ \to R Fr A$
23	5	a1i	$⊢ ⊤ \to S Fr B$
24	8	a1i	$⊢ ⊤ \to T Fr C$
25	1 22 23 24	frxp3	$⊢ ⊤ \to U Fr ((A \times B) \times C)$
26	25	mptru	$⊢ U Fr ((A \times B) \times C)$
27	3	a1i	$⊢ ⊤ \to R Po A$
28	6	a1i	$⊢ ⊤ \to S Po B$
29	9	a1i	$⊢ ⊤ \to T Po C$
30	1 27 28 29	poxp3	$⊢ ⊤ \to U Po ((A \times B) \times C)$
31	30	mptru	$⊢ U Po ((A \times B) \times C)$
32	4	a1i	$⊢ ⊤ \to R Se A$
33	7	a1i	$⊢ ⊤ \to S Se B$
34	10	a1i	$⊢ ⊤ \to T Se C$
35	1 32 33 34	sexp3	$⊢ ⊤ \to U Se ((A \times B) \times C)$
36	35	mptru	$⊢ U Se ((A \times B) \times C)$
37	26 31 36	3pm3.2i	$⊢ (U Fr ((A \times B) \times C) \land U Po ((A \times B) \times C) \land U Se ((A \times B) \times C))$
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	eleq2d	$⊢ (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⟩\}))$
40	39	imbi1d	$⊢ (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 θ))$
41		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⟩)$
42		ot2elxp	$⊢ ⟨⟨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\}))$
43		vex	$⊢ d \in V$
44		vex	$⊢ e \in V$
45		vex	$⊢ f \in V$
46	43 44 45	otthne	$⊢ ⟨⟨d, e⟩, f⟩ \neq ⟨⟨a, b⟩, c⟩ \leftrightarrow (d \neq a \lor e \neq b \lor f \neq c)$
47	42 46	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))$
48	41 47	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))$
49	48	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 θ)$
50		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 θ))$
51	49 50	bitr2i	$⊢ ((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 (⟨⟨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 θ)$
52	40 51	bitr4di	$⊢ (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 θ)))$
53	52	albidv	$⊢ (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 θ)))$
54	53	2albidv	$⊢ (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 θ)))$
55		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 θ))$
56	54 55	bitr4di	$⊢ (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 θ))$
57		ssun1	$⊢ Pred (R, A, a) \subseteq Pred (R, A, a) \cup \{a\}$
58		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) \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) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
59	57 58	ax-mp	$⊢ \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) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
60		ssun1	$⊢ Pred (S, B, b) \subseteq Pred (S, B, b) \cup \{b\}$
61		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) \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) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
62	60 61	ax-mp	$⊢ \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) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
63		ssun1	$⊢ Pred (T, C, c) \subseteq Pred (T, C, c) \cup \{c\}$
64		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 θ))$
65	63 64	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 θ)$
66	65	ralimi	$⊢ \forall e \in Pred (S, B, 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	62 66	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 θ)$
68	67	ralimi	$⊢ \forall d \in Pred (R, A, 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 θ)$
69		predpoirr	$⊢ T Po C \to \neg c \in Pred (T, C, c)$
70	9 69	ax-mp	$⊢ \neg c \in Pred (T, C, c)$
71		eleq1w	$⊢ f = c \to (f \in Pred (T, C, c) \leftrightarrow c \in Pred (T, C, c))$
72	70 71	mtbiri	$⊢ f = c \to \neg f \in Pred (T, C, c)$
73	72	necon2ai	$⊢ f \in Pred (T, C, c) \to f \neq c$
74	73	3mix3d	$⊢ f \in Pred (T, C, c) \to (d \neq a \lor e \neq b \lor f \neq c)$
75		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 θ)$
76	74 75	syl	$⊢ f \in Pred (T, C, c) \to (((d \neq a \lor e \neq b \lor f \neq c) \to θ) \to θ)$
77	76	ralimia	$⊢ \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) θ$
78	77	2ralimi	$⊢ \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) θ$
79	59 68 78	3syl	$⊢ \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) θ$
80		ssun2	$⊢ \{c\} \subseteq Pred (T, C, c) \cup \{c\}$
81		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 θ))$
82	80 81	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 θ)$
83	82	ralimi	$⊢ \forall e \in Pred (S, B, 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 θ)$
84	62 83	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 θ)$
85	84	ralimi	$⊢ \forall d \in Pred (R, A, 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 θ)$
86	59 85	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 θ)$
87		vex	$⊢ c \in V$
88		biidd	$⊢ f = c \to (d \neq a \leftrightarrow d \neq a)$
89		biidd	$⊢ f = c \to (e \neq b \leftrightarrow e \neq b)$
90		neeq1	$⊢ f = c \to (f \neq c \leftrightarrow c \neq c)$
91	88 89 90	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))$
92	13	bicomd	$⊢ c = f \to (θ \leftrightarrow χ)$
93	92	equcoms	$⊢ f = c \to (θ \leftrightarrow χ)$
94	91 93	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 χ))$
95	87 94	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 χ)$
96	95	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 χ)$
97	86 96	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 χ)$
98		predpoirr	$⊢ S Po B \to \neg b \in Pred (S, B, b)$
99	6 98	ax-mp	$⊢ \neg b \in Pred (S, B, b)$
100		eleq1w	$⊢ e = b \to (e \in Pred (S, B, b) \leftrightarrow b \in Pred (S, B, b))$
101	99 100	mtbiri	$⊢ e = b \to \neg e \in Pred (S, B, b)$
102	101	necon2ai	$⊢ e \in Pred (S, B, b) \to e \neq b$
103	102	3mix2d	$⊢ e \in Pred (S, B, b) \to (d \neq a \lor e \neq b \lor c \neq c)$
104		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 χ)$
105	103 104	syl	$⊢ e \in Pred (S, B, b) \to (((d \neq a \lor e \neq b \lor c \neq c) \to χ) \to χ)$
106	105	ralimia	$⊢ \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) χ$
107	106	ralimi	$⊢ \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) χ$
108	97 107	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) χ$
109		ssun2	$⊢ \{b\} \subseteq Pred (S, B, b) \cup \{b\}$
110		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) \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) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
111	109 110	ax-mp	$⊢ \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) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
112	65	ralimi	$⊢ \forall e \in \{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 θ)$
113	111 112	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 θ)$
114	113	ralimi	$⊢ \forall d \in Pred (R, A, 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 θ)$
115	59 114	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 θ)$
116		vex	$⊢ b \in V$
117		biidd	$⊢ e = b \to (d \neq a \leftrightarrow d \neq a)$
118		neeq1	$⊢ e = b \to (e \neq b \leftrightarrow b \neq b)$
119		biidd	$⊢ e = b \to (f \neq c \leftrightarrow f \neq c)$
120	117 118 119	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))$
121		equcom	$⊢ b = e \leftrightarrow e = b$
122		bicom	$⊢ (ζ \leftrightarrow θ) \leftrightarrow (θ \leftrightarrow ζ)$
123	16 121 122	3imtr3i	$⊢ e = b \to (θ \leftrightarrow ζ)$
124	120 123	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 ζ))$
125	124	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 ζ))$
126	116 125	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 ζ)$
127	126	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 ζ)$
128	115 127	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 ζ)$
129	73	3mix3d	$⊢ f \in Pred (T, C, c) \to (d \neq a \lor b \neq b \lor f \neq c)$
130		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 ζ)$
131	129 130	syl	$⊢ f \in Pred (T, C, c) \to (((d \neq a \lor b \neq b \lor f \neq c) \to ζ) \to ζ)$
132	131	ralimia	$⊢ \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) ζ$
133	132	ralimi	$⊢ \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) ζ$
134	128 133	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 f \in Pred (T, C, c) ζ$
135	79 108 134	3jca	$⊢ \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) ζ)$
136	82	ralimi	$⊢ \forall e \in \{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 θ)$
137	111 136	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 θ)$
138	137	ralimi	$⊢ \forall d \in Pred (R, A, 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 θ)$
139	59 138	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 θ)$
140	95	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 χ)$
141		biidd	$⊢ e = b \to (c \neq c \leftrightarrow c \neq c)$
142	117 118 141	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))$
143	12	bicomd	$⊢ b = e \to (χ \leftrightarrow ψ)$
144	143	equcoms	$⊢ e = b \to (χ \leftrightarrow ψ)$
145	142 144	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 ψ))$
146	116 145	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 ψ)$
147	140 146	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 ψ)$
148	147	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 ψ)$
149	139 148	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 ψ)$
150		predpoirr	$⊢ R Po A \to \neg a \in Pred (R, A, a)$
151	3 150	ax-mp	$⊢ \neg a \in Pred (R, A, a)$
152		eleq1w	$⊢ d = a \to (d \in Pred (R, A, a) \leftrightarrow a \in Pred (R, A, a))$
153	151 152	mtbiri	$⊢ d = a \to \neg d \in Pred (R, A, a)$
154	153	necon2ai	$⊢ d \in Pred (R, A, a) \to d \neq a$
155	154	3mix1d	$⊢ d \in Pred (R, A, a) \to (d \neq a \lor b \neq b \lor c \neq c)$
156		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 ψ)$
157	155 156	syl	$⊢ d \in Pred (R, A, a) \to (((d \neq a \lor b \neq b \lor c \neq c) \to ψ) \to ψ)$
158	157	ralimia	$⊢ \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) ψ$
159	149 158	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) ψ$
160		ssun2	$⊢ \{a\} \subseteq Pred (R, A, a) \cup \{a\}$
161		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) \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) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ))$
162	160 161	ax-mp	$⊢ \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) \cup \{b\}) \forall f \in (Pred (T, C, c) \cup \{c\}) ((d \neq a \lor e \neq b \lor f \neq c) \to θ)$
163	67	ralimi	$⊢ \forall d \in \{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 θ)$
164	162 163	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 θ)$
165		vex	$⊢ a \in V$
166		neeq1	$⊢ d = a \to (d \neq a \leftrightarrow a \neq a)$
167		biidd	$⊢ d = a \to (e \neq b \leftrightarrow e \neq b)$
168		biidd	$⊢ d = a \to (f \neq c \leftrightarrow f \neq c)$
169	166 167 168	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))$
170	14	equcoms	$⊢ d = a \to (τ \leftrightarrow θ)$
171	170	bicomd	$⊢ d = a \to (θ \leftrightarrow τ)$
172	169 171	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 τ))$
173	172	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 τ))$
174	165 173	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 τ)$
175	164 174	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 τ)$
176	73	3mix3d	$⊢ f \in Pred (T, C, c) \to (a \neq a \lor e \neq b \lor f \neq c)$
177		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 τ)$
178	176 177	syl	$⊢ f \in Pred (T, C, c) \to (((a \neq a \lor e \neq b \lor f \neq c) \to τ) \to τ)$
179	178	ralimia	$⊢ \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) τ$
180	179	ralimi	$⊢ \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) τ$
181	175 180	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 e \in Pred (S, B, b) \forall f \in Pred (T, C, c) τ$
182	84	ralimi	$⊢ \forall d \in \{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 θ)$
183	162 182	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 θ)$
184	172	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 τ))$
185	165 184	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 τ)$
186		biidd	$⊢ f = c \to (a \neq a \leftrightarrow a \neq a)$
187	186 89 90	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))$
188	17	bicomd	$⊢ c = f \to (τ \leftrightarrow σ)$
189	188	equcoms	$⊢ f = c \to (τ \leftrightarrow σ)$
190	187 189	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 σ))$
191	87 190	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 σ)$
192	191	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 σ)$
193	185 192	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 σ)$
194	183 193	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 σ)$
195	102	3mix2d	$⊢ e \in Pred (S, B, b) \to (a \neq a \lor e \neq b \lor c \neq c)$
196		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 σ)$
197	195 196	syl	$⊢ e \in Pred (S, B, b) \to (((a \neq a \lor e \neq b \lor c \neq c) \to σ) \to σ)$
198	197	ralimia	$⊢ \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) σ$
199	194 198	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 e \in Pred (S, B, b) σ$
200	159 181 199	3jca	$⊢ \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) σ)$
201	113	ralimi	$⊢ \forall d \in \{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 θ)$
202	162 201	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 θ)$
203	172	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 τ))$
204	165 203	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 τ)$
205		biidd	$⊢ e = b \to (a \neq a \leftrightarrow a \neq a)$
206	205 118 119	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))$
207	15	equcoms	$⊢ e = b \to (η \leftrightarrow τ)$
208	207	bicomd	$⊢ e = b \to (τ \leftrightarrow η)$
209	206 208	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 η))$
210	209	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 η))$
211	116 210	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 η)$
212	204 211	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 η)$
213	202 212	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 η)$
214	73	3mix3d	$⊢ f \in Pred (T, C, c) \to (a \neq a \lor b \neq b \lor f \neq c)$
215		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 η)$
216	214 215	syl	$⊢ f \in Pred (T, C, c) \to (((a \neq a \lor b \neq b \lor f \neq c) \to η) \to η)$
217	216	ralimia	$⊢ \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) η$
218	213 217	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 f \in Pred (T, C, c) η$
219	135 200 218	3jca	$⊢ \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) η)$
220	219 21	syl5	$⊢ (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 φ)$
221	56 220	sylbid	$⊢ (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 φ)$
222	221 11 12 13 18 19 20	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 λ$
223	37 222	mpan	$⊢ (X \in A \land Y \in B \land Z \in C) \to λ$

Metamath Proof Explorer

Theorem xpord3ind

Proof