poxp3

Description: Triple Cartesian product partial ordering. (Contributed by Scott Fenton, 21-Aug-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))\}$
	poxp3.1	$⊢ φ \to R Po A$
	poxp3.2	$⊢ φ \to S Po B$
	poxp3.3	$⊢ φ \to T Po C$
Assertion	poxp3	$⊢ φ \to U Po ((A \times B) \times C)$

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		poxp3.1	$⊢ φ \to R Po A$
3		poxp3.2	$⊢ φ \to S Po B$
4		poxp3.3	$⊢ φ \to T Po C$
5		el2xptp	$⊢ p \in ((A \times B) \times C) \leftrightarrow \exists a \in A \exists b \in B \exists c \in C p = ⟨a, b, c⟩$
6		neirr	$⊢ \neg a \neq a$
7		neirr	$⊢ \neg b \neq b$
8		neirr	$⊢ \neg c \neq c$
9	6 7 8	3pm3.2ni	$⊢ \neg (a \neq a \lor b \neq b \lor c \neq c)$
10	9	intnan	$⊢ \neg (((a R a \lor a = a) \land (b S b \lor b = b) \land (c T c \lor c = c)) \land (a \neq a \lor b \neq b \lor c \neq c))$
11		simp3	$⊢ ((a \in A \land b \in B \land c \in C) \land (a \in A \land b \in B \land c \in C) \land (((a R a \lor a = a) \land (b S b \lor b = b) \land (c T c \lor c = c)) \land (a \neq a \lor b \neq b \lor c \neq c))) \to (((a R a \lor a = a) \land (b S b \lor b = b) \land (c T c \lor c = c)) \land (a \neq a \lor b \neq b \lor c \neq c))$
12	10 11	mto	$⊢ \neg ((a \in A \land b \in B \land c \in C) \land (a \in A \land b \in B \land c \in C) \land (((a R a \lor a = a) \land (b S b \lor b = b) \land (c T c \lor c = c)) \land (a \neq a \lor b \neq b \lor c \neq c)))$
13		breq12	$⊢ (p = ⟨a, b, c⟩ \land p = ⟨a, b, c⟩) \to (p U p \leftrightarrow ⟨a, b, c⟩ U ⟨a, b, c⟩)$
14	13	anidms	$⊢ p = ⟨a, b, c⟩ \to (p U p \leftrightarrow ⟨a, b, c⟩ U ⟨a, b, c⟩)$
15	1	xpord3lem	$⊢ ⟨a, b, c⟩ U ⟨a, b, c⟩ \leftrightarrow ((a \in A \land b \in B \land c \in C) \land (a \in A \land b \in B \land c \in C) \land (((a R a \lor a = a) \land (b S b \lor b = b) \land (c T c \lor c = c)) \land (a \neq a \lor b \neq b \lor c \neq c)))$
16	14 15	bitrdi	$⊢ p = ⟨a, b, c⟩ \to (p U p \leftrightarrow ((a \in A \land b \in B \land c \in C) \land (a \in A \land b \in B \land c \in C) \land (((a R a \lor a = a) \land (b S b \lor b = b) \land (c T c \lor c = c)) \land (a \neq a \lor b \neq b \lor c \neq c))))$
17	12 16	mtbiri	$⊢ p = ⟨a, b, c⟩ \to \neg p U p$
18	17	rexlimivw	$⊢ \exists c \in C p = ⟨a, b, c⟩ \to \neg p U p$
19	18	rexlimivw	$⊢ \exists b \in B \exists c \in C p = ⟨a, b, c⟩ \to \neg p U p$
20	19	rexlimivw	$⊢ \exists a \in A \exists b \in B \exists c \in C p = ⟨a, b, c⟩ \to \neg p U p$
21	5 20	sylbi	$⊢ p \in ((A \times B) \times C) \to \neg p U p$
22	21	adantl	$⊢ (φ \land p \in ((A \times B) \times C)) \to \neg p U p$
23		3reeanv	$⊢ \exists a \in A \exists d \in A \exists g \in A (\exists b \in B \exists c \in C p = ⟨a, b, c⟩ \land \exists e \in B \exists f \in C q = ⟨d, e, f⟩ \land \exists h \in B \exists i \in C r = ⟨g, h, i⟩) \leftrightarrow (\exists a \in A \exists b \in B \exists c \in C p = ⟨a, b, c⟩ \land \exists d \in A \exists e \in B \exists f \in C q = ⟨d, e, f⟩ \land \exists g \in A \exists h \in B \exists i \in C r = ⟨g, h, i⟩)$
24		3reeanv	$⊢ \exists c \in C \exists f \in C \exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \leftrightarrow (\exists c \in C p = ⟨a, b, c⟩ \land \exists f \in C q = ⟨d, e, f⟩ \land \exists i \in C r = ⟨g, h, i⟩)$
25	24	rexbii	$⊢ \exists h \in B \exists c \in C \exists f \in C \exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \leftrightarrow \exists h \in B (\exists c \in C p = ⟨a, b, c⟩ \land \exists f \in C q = ⟨d, e, f⟩ \land \exists i \in C r = ⟨g, h, i⟩)$
26	25	2rexbii	$⊢ \exists b \in B \exists e \in B \exists h \in B \exists c \in C \exists f \in C \exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \leftrightarrow \exists b \in B \exists e \in B \exists h \in B (\exists c \in C p = ⟨a, b, c⟩ \land \exists f \in C q = ⟨d, e, f⟩ \land \exists i \in C r = ⟨g, h, i⟩)$
27		3reeanv	$⊢ \exists b \in B \exists e \in B \exists h \in B (\exists c \in C p = ⟨a, b, c⟩ \land \exists f \in C q = ⟨d, e, f⟩ \land \exists i \in C r = ⟨g, h, i⟩) \leftrightarrow (\exists b \in B \exists c \in C p = ⟨a, b, c⟩ \land \exists e \in B \exists f \in C q = ⟨d, e, f⟩ \land \exists h \in B \exists i \in C r = ⟨g, h, i⟩)$
28	26 27	bitri	$⊢ \exists b \in B \exists e \in B \exists h \in B \exists c \in C \exists f \in C \exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \leftrightarrow (\exists b \in B \exists c \in C p = ⟨a, b, c⟩ \land \exists e \in B \exists f \in C q = ⟨d, e, f⟩ \land \exists h \in B \exists i \in C r = ⟨g, h, i⟩)$
29	28	rexbii	$⊢ \exists g \in A \exists b \in B \exists e \in B \exists h \in B \exists c \in C \exists f \in C \exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \leftrightarrow \exists g \in A (\exists b \in B \exists c \in C p = ⟨a, b, c⟩ \land \exists e \in B \exists f \in C q = ⟨d, e, f⟩ \land \exists h \in B \exists i \in C r = ⟨g, h, i⟩)$
30	29	2rexbii	$⊢ \exists a \in A \exists d \in A \exists g \in A \exists b \in B \exists e \in B \exists h \in B \exists c \in C \exists f \in C \exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \leftrightarrow \exists a \in A \exists d \in A \exists g \in A (\exists b \in B \exists c \in C p = ⟨a, b, c⟩ \land \exists e \in B \exists f \in C q = ⟨d, e, f⟩ \land \exists h \in B \exists i \in C r = ⟨g, h, i⟩)$
31		el2xptp	$⊢ q \in ((A \times B) \times C) \leftrightarrow \exists d \in A \exists e \in B \exists f \in C q = ⟨d, e, f⟩$
32		el2xptp	$⊢ r \in ((A \times B) \times C) \leftrightarrow \exists g \in A \exists h \in B \exists i \in C r = ⟨g, h, i⟩$
33	5 31 32	3anbi123i	$⊢ (p \in ((A \times B) \times C) \land q \in ((A \times B) \times C) \land r \in ((A \times B) \times C)) \leftrightarrow (\exists a \in A \exists b \in B \exists c \in C p = ⟨a, b, c⟩ \land \exists d \in A \exists e \in B \exists f \in C q = ⟨d, e, f⟩ \land \exists g \in A \exists h \in B \exists i \in C r = ⟨g, h, i⟩)$
34	23 30 33	3bitr4ri	$⊢ (p \in ((A \times B) \times C) \land q \in ((A \times B) \times C) \land r \in ((A \times B) \times C)) \leftrightarrow \exists a \in A \exists d \in A \exists g \in A \exists b \in B \exists e \in B \exists h \in B \exists c \in C \exists f \in C \exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩)$
35		simpr1l	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (a \in A \land b \in B \land c \in C)$
36		simpr2r	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (g \in A \land h \in B \land i \in C)$
37		simp1l1	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to a \in A$
38		simp2l1	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to d \in A$
39		simp2r1	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to g \in A$
40	37 38 39	3jca	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to (a \in A \land d \in A \land g \in A)$
41		potr	$⊢ (R Po A \land (a \in A \land d \in A \land g \in A)) \to ((a R d \land d R g) \to a R g)$
42	2 40 41	syl2an	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to ((a R d \land d R g) \to a R g)$
43	42	expd	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (a R d \to (d R g \to a R g))$
44		breq1	$⊢ a = d \to (a R g \leftrightarrow d R g)$
45	44	biimprd	$⊢ a = d \to (d R g \to a R g)$
46	45	a1i	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (a = d \to (d R g \to a R g))$
47		simpll1	$⊢ ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))) \to (a R d \lor a = d)$
48	47	3ad2ant3	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to (a R d \lor a = d)$
49	48	adantl	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (a R d \lor a = d)$
50	43 46 49	mpjaod	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (d R g \to a R g)$
51		orc	$⊢ a R g \to (a R g \lor a = g)$
52	50 51	syl6	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (d R g \to (a R g \lor a = g))$
53		breq2	$⊢ d = g \to (a R d \leftrightarrow a R g)$
54		equequ2	$⊢ d = g \to (a = d \leftrightarrow a = g)$
55	53 54	orbi12d	$⊢ d = g \to ((a R d \lor a = d) \leftrightarrow (a R g \lor a = g))$
56	49 55	syl5ibcom	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (d = g \to (a R g \lor a = g))$
57		simprl1	$⊢ ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))) \to (d R g \lor d = g)$
58	57	3ad2ant3	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to (d R g \lor d = g)$
59	58	adantl	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (d R g \lor d = g)$
60	52 56 59	mpjaod	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (a R g \lor a = g)$
61		simp1l2	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to b \in B$
62		simp2l2	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to e \in B$
63		simp2r2	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to h \in B$
64	61 62 63	3jca	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to (b \in B \land e \in B \land h \in B)$
65		potr	$⊢ (S Po B \land (b \in B \land e \in B \land h \in B)) \to ((b S e \land e S h) \to b S h)$
66	3 64 65	syl2an	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to ((b S e \land e S h) \to b S h)$
67	66	expd	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (b S e \to (e S h \to b S h))$
68		breq1	$⊢ b = e \to (b S h \leftrightarrow e S h)$
69	68	biimprd	$⊢ b = e \to (e S h \to b S h)$
70	69	a1i	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (b = e \to (e S h \to b S h))$
71		simpll2	$⊢ ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))) \to (b S e \lor b = e)$
72	71	3ad2ant3	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to (b S e \lor b = e)$
73	72	adantl	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (b S e \lor b = e)$
74	67 70 73	mpjaod	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (e S h \to b S h)$
75		orc	$⊢ b S h \to (b S h \lor b = h)$
76	74 75	syl6	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (e S h \to (b S h \lor b = h))$
77		breq2	$⊢ e = h \to (b S e \leftrightarrow b S h)$
78		equequ2	$⊢ e = h \to (b = e \leftrightarrow b = h)$
79	77 78	orbi12d	$⊢ e = h \to ((b S e \lor b = e) \leftrightarrow (b S h \lor b = h))$
80	73 79	syl5ibcom	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (e = h \to (b S h \lor b = h))$
81		simprl2	$⊢ ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))) \to (e S h \lor e = h)$
82	81	3ad2ant3	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to (e S h \lor e = h)$
83	82	adantl	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (e S h \lor e = h)$
84	76 80 83	mpjaod	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (b S h \lor b = h)$
85		simp1l3	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to c \in C$
86		simp2l3	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to f \in C$
87		simp2r3	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to i \in C$
88	85 86 87	3jca	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to (c \in C \land f \in C \land i \in C)$
89		potr	$⊢ (T Po C \land (c \in C \land f \in C \land i \in C)) \to ((c T f \land f T i) \to c T i)$
90	4 88 89	syl2an	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to ((c T f \land f T i) \to c T i)$
91	90	expd	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (c T f \to (f T i \to c T i))$
92		breq1	$⊢ c = f \to (c T i \leftrightarrow f T i)$
93	92	biimprd	$⊢ c = f \to (f T i \to c T i)$
94	93	a1i	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (c = f \to (f T i \to c T i))$
95		simpll3	$⊢ ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))) \to (c T f \lor c = f)$
96	95	3ad2ant3	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to (c T f \lor c = f)$
97	96	adantl	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (c T f \lor c = f)$
98	91 94 97	mpjaod	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (f T i \to c T i)$
99		orc	$⊢ c T i \to (c T i \lor c = i)$
100	98 99	syl6	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (f T i \to (c T i \lor c = i))$
101		breq2	$⊢ f = i \to (c T f \leftrightarrow c T i)$
102		equequ2	$⊢ f = i \to (c = f \leftrightarrow c = i)$
103	101 102	orbi12d	$⊢ f = i \to ((c T f \lor c = f) \leftrightarrow (c T i \lor c = i))$
104	97 103	syl5ibcom	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (f = i \to (c T i \lor c = i))$
105		simprl3	$⊢ ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))) \to (f T i \lor f = i)$
106	105	3ad2ant3	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to (f T i \lor f = i)$
107	106	adantl	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (f T i \lor f = i)$
108	100 104 107	mpjaod	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (c T i \lor c = i)$
109	60 84 108	3jca	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to ((a R g \lor a = g) \land (b S h \lor b = h) \land (c T i \lor c = i))$
110		simp3rr	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to (d \neq g \lor e \neq h \lor f \neq i)$
111	110	adantl	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (d \neq g \lor e \neq h \lor f \neq i)$
112	59	adantr	$⊢ ((φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \land a = g) \to (d R g \lor d = g)$
113		breq1	$⊢ a = g \to (a R d \leftrightarrow g R d)$
114		equequ1	$⊢ a = g \to (a = d \leftrightarrow g = d)$
115		equcom	$⊢ g = d \leftrightarrow d = g$
116	114 115	bitrdi	$⊢ a = g \to (a = d \leftrightarrow d = g)$
117	113 116	orbi12d	$⊢ a = g \to ((a R d \lor a = d) \leftrightarrow (g R d \lor d = g))$
118	49 117	syl5ibcom	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (a = g \to (g R d \lor d = g))$
119	118	imp	$⊢ ((φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \land a = g) \to (g R d \lor d = g)$
120		ordir	$⊢ ((d R g \land g R d) \lor d = g) \leftrightarrow ((d R g \lor d = g) \land (g R d \lor d = g))$
121	112 119 120	sylanbrc	$⊢ ((φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \land a = g) \to ((d R g \land g R d) \lor d = g)$
122	2	adantr	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to R Po A$
123	38	adantl	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to d \in A$
124	39	adantl	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to g \in A$
125		po2nr	$⊢ (R Po A \land (d \in A \land g \in A)) \to \neg (d R g \land g R d)$
126	122 123 124 125	syl12anc	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to \neg (d R g \land g R d)$
127	126	adantr	$⊢ ((φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \land a = g) \to \neg (d R g \land g R d)$
128	121 127	orcnd	$⊢ ((φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \land a = g) \to d = g$
129	128	ex	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (a = g \to d = g)$
130	129	necon3d	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (d \neq g \to a \neq g)$
131	83	adantr	$⊢ ((φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \land b = h) \to (e S h \lor e = h)$
132		breq1	$⊢ b = h \to (b S e \leftrightarrow h S e)$
133		equequ1	$⊢ b = h \to (b = e \leftrightarrow h = e)$
134		equcom	$⊢ h = e \leftrightarrow e = h$
135	133 134	bitrdi	$⊢ b = h \to (b = e \leftrightarrow e = h)$
136	132 135	orbi12d	$⊢ b = h \to ((b S e \lor b = e) \leftrightarrow (h S e \lor e = h))$
137	73 136	syl5ibcom	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (b = h \to (h S e \lor e = h))$
138	137	imp	$⊢ ((φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \land b = h) \to (h S e \lor e = h)$
139		ordir	$⊢ ((e S h \land h S e) \lor e = h) \leftrightarrow ((e S h \lor e = h) \land (h S e \lor e = h))$
140	131 138 139	sylanbrc	$⊢ ((φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \land b = h) \to ((e S h \land h S e) \lor e = h)$
141	3	adantr	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to S Po B$
142	62	adantl	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to e \in B$
143	63	adantl	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to h \in B$
144		po2nr	$⊢ (S Po B \land (e \in B \land h \in B)) \to \neg (e S h \land h S e)$
145	141 142 143 144	syl12anc	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to \neg (e S h \land h S e)$
146	145	adantr	$⊢ ((φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \land b = h) \to \neg (e S h \land h S e)$
147	140 146	orcnd	$⊢ ((φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \land b = h) \to e = h$
148	147	ex	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (b = h \to e = h)$
149	148	necon3d	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (e \neq h \to b \neq h)$
150	107	adantr	$⊢ ((φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \land c = i) \to (f T i \lor f = i)$
151		breq1	$⊢ c = i \to (c T f \leftrightarrow i T f)$
152		equequ1	$⊢ c = i \to (c = f \leftrightarrow i = f)$
153		equcom	$⊢ i = f \leftrightarrow f = i$
154	152 153	bitrdi	$⊢ c = i \to (c = f \leftrightarrow f = i)$
155	151 154	orbi12d	$⊢ c = i \to ((c T f \lor c = f) \leftrightarrow (i T f \lor f = i))$
156	97 155	syl5ibcom	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (c = i \to (i T f \lor f = i))$
157	156	imp	$⊢ ((φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \land c = i) \to (i T f \lor f = i)$
158		ordir	$⊢ ((f T i \land i T f) \lor f = i) \leftrightarrow ((f T i \lor f = i) \land (i T f \lor f = i))$
159	150 157 158	sylanbrc	$⊢ ((φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \land c = i) \to ((f T i \land i T f) \lor f = i)$
160	4	adantr	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to T Po C$
161	86	adantl	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to f \in C$
162	87	adantl	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to i \in C$
163		po2nr	$⊢ (T Po C \land (f \in C \land i \in C)) \to \neg (f T i \land i T f)$
164	160 161 162 163	syl12anc	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to \neg (f T i \land i T f)$
165	164	adantr	$⊢ ((φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \land c = i) \to \neg (f T i \land i T f)$
166	159 165	orcnd	$⊢ ((φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \land c = i) \to f = i$
167	166	ex	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (c = i \to f = i)$
168	167	necon3d	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (f \neq i \to c \neq i)$
169	130 149 168	3orim123d	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to ((d \neq g \lor e \neq h \lor f \neq i) \to (a \neq g \lor b \neq h \lor c \neq i))$
170	111 169	mpd	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (a \neq g \lor b \neq h \lor c \neq i)$
171	109 170	jca	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to (((a R g \lor a = g) \land (b S h \lor b = h) \land (c T i \lor c = i)) \land (a \neq g \lor b \neq h \lor c \neq i))$
172	35 36 171	3jca	$⊢ (φ \land (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))) \to ((a \in A \land b \in B \land c \in C) \land (g \in A \land h \in B \land i \in C) \land (((a R g \lor a = g) \land (b S h \lor b = h) \land (c T i \lor c = i)) \land (a \neq g \lor b \neq h \lor c \neq i)))$
173	172	ex	$⊢ φ \to ((((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to ((a \in A \land b \in B \land c \in C) \land (g \in A \land h \in B \land i \in C) \land (((a R g \lor a = g) \land (b S h \lor b = h) \land (c T i \lor c = i)) \land (a \neq g \lor b \neq h \lor c \neq i))))$
174		breq12	$⊢ (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩) \to (p U q \leftrightarrow ⟨a, b, c⟩ U ⟨d, e, f⟩)$
175	174	3adant3	$⊢ (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to (p U q \leftrightarrow ⟨a, b, c⟩ U ⟨d, e, f⟩)$
176	1	xpord3lem	$⊢ ⟨a, b, c⟩ U ⟨d, e, f⟩ \leftrightarrow ((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C) \land (((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)))$
177	175 176	bitrdi	$⊢ (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to (p U q \leftrightarrow ((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C) \land (((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f))))$
178		breq12	$⊢ (q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to (q U r \leftrightarrow ⟨d, e, f⟩ U ⟨g, h, i⟩)$
179	178	3adant1	$⊢ (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to (q U r \leftrightarrow ⟨d, e, f⟩ U ⟨g, h, i⟩)$
180	1	xpord3lem	$⊢ ⟨d, e, f⟩ U ⟨g, h, i⟩ \leftrightarrow ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))$
181	179 180	bitrdi	$⊢ (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to (q U r \leftrightarrow ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))$
182	177 181	anbi12d	$⊢ (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to ((p U q \land q U r) \leftrightarrow (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C) \land (((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f))) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))))$
183		an6	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C) \land (((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f))) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \leftrightarrow (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i))))$
184	182 183	bitrdi	$⊢ (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to ((p U q \land q U r) \leftrightarrow (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))))$
185		breq12	$⊢ (p = ⟨a, b, c⟩ \land r = ⟨g, h, i⟩) \to (p U r \leftrightarrow ⟨a, b, c⟩ U ⟨g, h, i⟩)$
186	185	3adant2	$⊢ (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to (p U r \leftrightarrow ⟨a, b, c⟩ U ⟨g, h, i⟩)$
187	1	xpord3lem	$⊢ ⟨a, b, c⟩ U ⟨g, h, i⟩ \leftrightarrow ((a \in A \land b \in B \land c \in C) \land (g \in A \land h \in B \land i \in C) \land (((a R g \lor a = g) \land (b S h \lor b = h) \land (c T i \lor c = i)) \land (a \neq g \lor b \neq h \lor c \neq i)))$
188	186 187	bitrdi	$⊢ (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to (p U r \leftrightarrow ((a \in A \land b \in B \land c \in C) \land (g \in A \land h \in B \land i \in C) \land (((a R g \lor a = g) \land (b S h \lor b = h) \land (c T i \lor c = i)) \land (a \neq g \lor b \neq h \lor c \neq i))))$
189	184 188	imbi12d	$⊢ (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to (((p U q \land q U r) \to p U r) \leftrightarrow ((((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C)) \land ((d \in A \land e \in B \land f \in C) \land (g \in A \land h \in B \land i \in C)) \land ((((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)) \land (((d R g \lor d = g) \land (e S h \lor e = h) \land (f T i \lor f = i)) \land (d \neq g \lor e \neq h \lor f \neq i)))) \to ((a \in A \land b \in B \land c \in C) \land (g \in A \land h \in B \land i \in C) \land (((a R g \lor a = g) \land (b S h \lor b = h) \land (c T i \lor c = i)) \land (a \neq g \lor b \neq h \lor c \neq i)))))$
190	173 189	syl5ibrcom	$⊢ φ \to ((p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to ((p U q \land q U r) \to p U r))$
191	190	rexlimdvw	$⊢ φ \to (\exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to ((p U q \land q U r) \to p U r))$
192	191	rexlimdvw	$⊢ φ \to (\exists f \in C \exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to ((p U q \land q U r) \to p U r))$
193	192	rexlimdvw	$⊢ φ \to (\exists c \in C \exists f \in C \exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to ((p U q \land q U r) \to p U r))$
194	193	rexlimdvw	$⊢ φ \to (\exists h \in B \exists c \in C \exists f \in C \exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to ((p U q \land q U r) \to p U r))$
195	194	rexlimdvw	$⊢ φ \to (\exists e \in B \exists h \in B \exists c \in C \exists f \in C \exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to ((p U q \land q U r) \to p U r))$
196	195	rexlimdvw	$⊢ φ \to (\exists b \in B \exists e \in B \exists h \in B \exists c \in C \exists f \in C \exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to ((p U q \land q U r) \to p U r))$
197	196	rexlimdvw	$⊢ φ \to (\exists g \in A \exists b \in B \exists e \in B \exists h \in B \exists c \in C \exists f \in C \exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to ((p U q \land q U r) \to p U r))$
198	197	rexlimdvw	$⊢ φ \to (\exists d \in A \exists g \in A \exists b \in B \exists e \in B \exists h \in B \exists c \in C \exists f \in C \exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to ((p U q \land q U r) \to p U r))$
199	198	rexlimdvw	$⊢ φ \to (\exists a \in A \exists d \in A \exists g \in A \exists b \in B \exists e \in B \exists h \in B \exists c \in C \exists f \in C \exists i \in C (p = ⟨a, b, c⟩ \land q = ⟨d, e, f⟩ \land r = ⟨g, h, i⟩) \to ((p U q \land q U r) \to p U r))$
200	34 199	biimtrid	$⊢ φ \to ((p \in ((A \times B) \times C) \land q \in ((A \times B) \times C) \land r \in ((A \times B) \times C)) \to ((p U q \land q U r) \to p U r))$
201	200	imp	$⊢ (φ \land (p \in ((A \times B) \times C) \land q \in ((A \times B) \times C) \land r \in ((A \times B) \times C))) \to ((p U q \land q U r) \to p U r)$
202	22 201	ispod	$⊢ φ \to U Po ((A \times B) \times C)$

Metamath Proof Explorer

Theorem poxp3

Proof