poxp3

Description: Triple cross 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		elxpxp	$⊢ a \in ((A \times B) \times C) \leftrightarrow \exists d \in A \exists e \in B \exists f \in C a = ⟨⟨d, e⟩, f⟩$
6		neirr	$⊢ \neg d \neq d$
7		neirr	$⊢ \neg e \neq e$
8		neirr	$⊢ \neg f \neq f$
9	6 7 8	3pm3.2ni	$⊢ \neg (d \neq d \lor e \neq e \lor f \neq f)$
10	9	intnan	$⊢ \neg (((d R d \lor d = d) \land (e S e \lor e = e) \land (f T f \lor f = f)) \land (d \neq d \lor e \neq e \lor f \neq f))$
11		simp3	$⊢ ((d \in A \land e \in B \land f \in C) \land (d \in A \land e \in B \land f \in C) \land (((d R d \lor d = d) \land (e S e \lor e = e) \land (f T f \lor f = f)) \land (d \neq d \lor e \neq e \lor f \neq f))) \to (((d R d \lor d = d) \land (e S e \lor e = e) \land (f T f \lor f = f)) \land (d \neq d \lor e \neq e \lor f \neq f))$
12	10 11	mto	$⊢ \neg ((d \in A \land e \in B \land f \in C) \land (d \in A \land e \in B \land f \in C) \land (((d R d \lor d = d) \land (e S e \lor e = e) \land (f T f \lor f = f)) \land (d \neq d \lor e \neq e \lor f \neq f)))$
13		breq12	$⊢ (a = ⟨⟨d, e⟩, f⟩ \land a = ⟨⟨d, e⟩, f⟩) \to (a U a \leftrightarrow ⟨⟨d, e⟩, f⟩ U ⟨⟨d, e⟩, f⟩)$
14	13	anidms	$⊢ a = ⟨⟨d, e⟩, f⟩ \to (a U a \leftrightarrow ⟨⟨d, e⟩, f⟩ U ⟨⟨d, e⟩, f⟩)$
15	1	xpord3lem	$⊢ ⟨⟨d, e⟩, f⟩ U ⟨⟨d, e⟩, f⟩ \leftrightarrow ((d \in A \land e \in B \land f \in C) \land (d \in A \land e \in B \land f \in C) \land (((d R d \lor d = d) \land (e S e \lor e = e) \land (f T f \lor f = f)) \land (d \neq d \lor e \neq e \lor f \neq f)))$
16	14 15	bitrdi	$⊢ a = ⟨⟨d, e⟩, f⟩ \to (a U a \leftrightarrow ((d \in A \land e \in B \land f \in C) \land (d \in A \land e \in B \land f \in C) \land (((d R d \lor d = d) \land (e S e \lor e = e) \land (f T f \lor f = f)) \land (d \neq d \lor e \neq e \lor f \neq f))))$
17	12 16	mtbiri	$⊢ a = ⟨⟨d, e⟩, f⟩ \to \neg a U a$
18	17	rexlimivw	$⊢ \exists f \in C a = ⟨⟨d, e⟩, f⟩ \to \neg a U a$
19	18	a1i	$⊢ (d \in A \land e \in B) \to (\exists f \in C a = ⟨⟨d, e⟩, f⟩ \to \neg a U a)$
20	19	rexlimivv	$⊢ \exists d \in A \exists e \in B \exists f \in C a = ⟨⟨d, e⟩, f⟩ \to \neg a U a$
21	5 20	sylbi	$⊢ a \in ((A \times B) \times C) \to \neg a U a$
22	21	adantl	$⊢ (φ \land a \in ((A \times B) \times C)) \to \neg a U a$
23		elxpxp	$⊢ b \in ((A \times B) \times C) \leftrightarrow \exists g \in A \exists h \in B \exists i \in C b = ⟨⟨g, h⟩, i⟩$
24		elxpxp	$⊢ c \in ((A \times B) \times C) \leftrightarrow \exists j \in A \exists k \in B \exists l \in C c = ⟨⟨j, k⟩, l⟩$
25	5 23 24	3anbi123i	$⊢ (a \in ((A \times B) \times C) \land b \in ((A \times B) \times C) \land c \in ((A \times B) \times C)) \leftrightarrow (\exists d \in A \exists e \in B \exists f \in C a = ⟨⟨d, e⟩, f⟩ \land \exists g \in A \exists h \in B \exists i \in C b = ⟨⟨g, h⟩, i⟩ \land \exists j \in A \exists k \in B \exists l \in C c = ⟨⟨j, k⟩, l⟩)$
26		3reeanv	$⊢ \exists f \in C \exists i \in C \exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \leftrightarrow (\exists f \in C a = ⟨⟨d, e⟩, f⟩ \land \exists i \in C b = ⟨⟨g, h⟩, i⟩ \land \exists l \in C c = ⟨⟨j, k⟩, l⟩)$
27	26	rexbii	$⊢ \exists k \in B \exists f \in C \exists i \in C \exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \leftrightarrow \exists k \in B (\exists f \in C a = ⟨⟨d, e⟩, f⟩ \land \exists i \in C b = ⟨⟨g, h⟩, i⟩ \land \exists l \in C c = ⟨⟨j, k⟩, l⟩)$
28	27	2rexbii	$⊢ \exists e \in B \exists h \in B \exists k \in B \exists f \in C \exists i \in C \exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \leftrightarrow \exists e \in B \exists h \in B \exists k \in B (\exists f \in C a = ⟨⟨d, e⟩, f⟩ \land \exists i \in C b = ⟨⟨g, h⟩, i⟩ \land \exists l \in C c = ⟨⟨j, k⟩, l⟩)$
29		3reeanv	$⊢ \exists e \in B \exists h \in B \exists k \in B (\exists f \in C a = ⟨⟨d, e⟩, f⟩ \land \exists i \in C b = ⟨⟨g, h⟩, i⟩ \land \exists l \in C c = ⟨⟨j, k⟩, l⟩) \leftrightarrow (\exists e \in B \exists f \in C a = ⟨⟨d, e⟩, f⟩ \land \exists h \in B \exists i \in C b = ⟨⟨g, h⟩, i⟩ \land \exists k \in B \exists l \in C c = ⟨⟨j, k⟩, l⟩)$
30	28 29	bitri	$⊢ \exists e \in B \exists h \in B \exists k \in B \exists f \in C \exists i \in C \exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \leftrightarrow (\exists e \in B \exists f \in C a = ⟨⟨d, e⟩, f⟩ \land \exists h \in B \exists i \in C b = ⟨⟨g, h⟩, i⟩ \land \exists k \in B \exists l \in C c = ⟨⟨j, k⟩, l⟩)$
31	30	rexbii	$⊢ \exists j \in A \exists e \in B \exists h \in B \exists k \in B \exists f \in C \exists i \in C \exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \leftrightarrow \exists j \in A (\exists e \in B \exists f \in C a = ⟨⟨d, e⟩, f⟩ \land \exists h \in B \exists i \in C b = ⟨⟨g, h⟩, i⟩ \land \exists k \in B \exists l \in C c = ⟨⟨j, k⟩, l⟩)$
32	31	2rexbii	$⊢ \exists d \in A \exists g \in A \exists j \in A \exists e \in B \exists h \in B \exists k \in B \exists f \in C \exists i \in C \exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \leftrightarrow \exists d \in A \exists g \in A \exists j \in A (\exists e \in B \exists f \in C a = ⟨⟨d, e⟩, f⟩ \land \exists h \in B \exists i \in C b = ⟨⟨g, h⟩, i⟩ \land \exists k \in B \exists l \in C c = ⟨⟨j, k⟩, l⟩)$
33		3reeanv	$⊢ \exists d \in A \exists g \in A \exists j \in A (\exists e \in B \exists f \in C a = ⟨⟨d, e⟩, f⟩ \land \exists h \in B \exists i \in C b = ⟨⟨g, h⟩, i⟩ \land \exists k \in B \exists l \in C c = ⟨⟨j, k⟩, l⟩) \leftrightarrow (\exists d \in A \exists e \in B \exists f \in C a = ⟨⟨d, e⟩, f⟩ \land \exists g \in A \exists h \in B \exists i \in C b = ⟨⟨g, h⟩, i⟩ \land \exists j \in A \exists k \in B \exists l \in C c = ⟨⟨j, k⟩, l⟩)$
34	32 33	bitri	$⊢ \exists d \in A \exists g \in A \exists j \in A \exists e \in B \exists h \in B \exists k \in B \exists f \in C \exists i \in C \exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \leftrightarrow (\exists d \in A \exists e \in B \exists f \in C a = ⟨⟨d, e⟩, f⟩ \land \exists g \in A \exists h \in B \exists i \in C b = ⟨⟨g, h⟩, i⟩ \land \exists j \in A \exists k \in B \exists l \in C c = ⟨⟨j, k⟩, l⟩)$
35	25 34	bitr4i	$⊢ (a \in ((A \times B) \times C) \land b \in ((A \times B) \times C) \land c \in ((A \times B) \times C)) \leftrightarrow \exists d \in A \exists g \in A \exists j \in A \exists e \in B \exists h \in B \exists k \in B \exists f \in C \exists i \in C \exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩)$
36		simprl1	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (d \in A \land e \in B \land f \in C)$
37		simprr2	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (j \in A \land k \in B \land l \in C)$
38	2	adantr	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to R Po A$
39		simpl11	$⊢ (((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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l)))) \to d \in A$
40	39	adantl	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to d \in A$
41		simpr11	$⊢ (((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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l)))) \to g \in A$
42	41	adantl	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to g \in A$
43		simpr21	$⊢ (((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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l)))) \to j \in A$
44	43	adantl	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to j \in A$
45		potr	$⊢ (R Po A \land (d \in A \land g \in A \land j \in A)) \to ((d R g \land g R j) \to d R j)$
46	38 40 42 44 45	syl13anc	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to ((d R g \land g R j) \to d R j)$
47		orc	$⊢ d R j \to (d R j \lor d = j)$
48	46 47	syl6	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to ((d R g \land g R j) \to (d R j \lor d = j))$
49	48	expd	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (d R g \to (g R j \to (d R j \lor d = j)))$
50		breq1	$⊢ d = g \to (d R j \leftrightarrow g R j)$
51	50 47	syl6bir	$⊢ d = g \to (g R j \to (d R j \lor d = j))$
52	51	a1i	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (d = g \to (g R j \to (d R j \lor d = j)))$
53		simp3l1	$⊢ ((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))) \to (d R g \lor d = g)$
54	53	ad2antrl	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (d R g \lor d = g)$
55	49 52 54	mpjaod	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (g R j \to (d R j \lor d = j))$
56		breq2	$⊢ g = j \to (d R g \leftrightarrow d R j)$
57		equequ2	$⊢ g = j \to (d = g \leftrightarrow d = j)$
58	56 57	orbi12d	$⊢ g = j \to ((d R g \lor d = g) \leftrightarrow (d R j \lor d = j))$
59	54 58	syl5ibcom	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (g = j \to (d R j \lor d = j))$
60		simp3l1	$⊢ ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))) \to (g R j \lor g = j)$
61	60	ad2antll	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (g R j \lor g = j)$
62	55 59 61	mpjaod	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (d R j \lor d = j)$
63	3	adantr	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to S Po B$
64		simpl12	$⊢ (((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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l)))) \to e \in B$
65	64	adantl	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to e \in B$
66		simpr12	$⊢ (((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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l)))) \to h \in B$
67	66	adantl	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to h \in B$
68		simpr22	$⊢ (((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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l)))) \to k \in B$
69	68	adantl	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to k \in B$
70		potr	$⊢ (S Po B \land (e \in B \land h \in B \land k \in B)) \to ((e S h \land h S k) \to e S k)$
71	63 65 67 69 70	syl13anc	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to ((e S h \land h S k) \to e S k)$
72		orc	$⊢ e S k \to (e S k \lor e = k)$
73	71 72	syl6	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to ((e S h \land h S k) \to (e S k \lor e = k))$
74	73	expd	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (e S h \to (h S k \to (e S k \lor e = k)))$
75		breq1	$⊢ e = h \to (e S k \leftrightarrow h S k)$
76	75 72	syl6bir	$⊢ e = h \to (h S k \to (e S k \lor e = k))$
77	76	a1i	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (e = h \to (h S k \to (e S k \lor e = k)))$
78		simp3l2	$⊢ ((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))) \to (e S h \lor e = h)$
79	78	ad2antrl	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (e S h \lor e = h)$
80	74 77 79	mpjaod	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (h S k \to (e S k \lor e = k))$
81		breq2	$⊢ h = k \to (e S h \leftrightarrow e S k)$
82		equequ2	$⊢ h = k \to (e = h \leftrightarrow e = k)$
83	81 82	orbi12d	$⊢ h = k \to ((e S h \lor e = h) \leftrightarrow (e S k \lor e = k))$
84	79 83	syl5ibcom	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (h = k \to (e S k \lor e = k))$
85		simp3l2	$⊢ ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))) \to (h S k \lor h = k)$
86	85	ad2antll	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (h S k \lor h = k)$
87	80 84 86	mpjaod	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (e S k \lor e = k)$
88	4	adantr	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to T Po C$
89		simpl13	$⊢ (((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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l)))) \to f \in C$
90	89	adantl	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to f \in C$
91		simpr13	$⊢ (((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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l)))) \to i \in C$
92	91	adantl	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to i \in C$
93		simpr23	$⊢ (((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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l)))) \to l \in C$
94	93	adantl	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to l \in C$
95		potr	$⊢ (T Po C \land (f \in C \land i \in C \land l \in C)) \to ((f T i \land i T l) \to f T l)$
96	88 90 92 94 95	syl13anc	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to ((f T i \land i T l) \to f T l)$
97		orc	$⊢ f T l \to (f T l \lor f = l)$
98	96 97	syl6	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to ((f T i \land i T l) \to (f T l \lor f = l))$
99	98	expd	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (f T i \to (i T l \to (f T l \lor f = l)))$
100		breq1	$⊢ f = i \to (f T l \leftrightarrow i T l)$
101	100 97	syl6bir	$⊢ f = i \to (i T l \to (f T l \lor f = l))$
102	101	a1i	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (f = i \to (i T l \to (f T l \lor f = l)))$
103		simp3l3	$⊢ ((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))) \to (f T i \lor f = i)$
104	103	ad2antrl	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (f T i \lor f = i)$
105	99 102 104	mpjaod	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (i T l \to (f T l \lor f = l))$
106		breq2	$⊢ i = l \to (f T i \leftrightarrow f T l)$
107		equequ2	$⊢ i = l \to (f = i \leftrightarrow f = l)$
108	106 107	orbi12d	$⊢ i = l \to ((f T i \lor f = i) \leftrightarrow (f T l \lor f = l))$
109	104 108	syl5ibcom	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (i = l \to (f T l \lor f = l))$
110		simp3l3	$⊢ ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))) \to (i T l \lor i = l)$
111	110	ad2antll	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (i T l \lor i = l)$
112	105 109 111	mpjaod	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (f T l \lor f = l)$
113	62 87 112	3jca	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to ((d R j \lor d = j) \land (e S k \lor e = k) \land (f T l \lor f = l))$
114		simpr3r	$⊢ (((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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l)))) \to (g \neq j \lor h \neq k \lor i \neq l)$
115	114	adantl	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (g \neq j \lor h \neq k \lor i \neq l)$
116		df-ne	$⊢ g \neq j \leftrightarrow \neg g = j$
117		df-ne	$⊢ h \neq k \leftrightarrow \neg h = k$
118		df-ne	$⊢ i \neq l \leftrightarrow \neg i = l$
119	116 117 118	3orbi123i	$⊢ (g \neq j \lor h \neq k \lor i \neq l) \leftrightarrow (\neg g = j \lor \neg h = k \lor \neg i = l)$
120		3ianor	$⊢ \neg (g = j \land h = k \land i = l) \leftrightarrow (\neg g = j \lor \neg h = k \lor \neg i = l)$
121	119 120	bitr4i	$⊢ (g \neq j \lor h \neq k \lor i \neq l) \leftrightarrow \neg (g = j \land h = k \land i = l)$
122	115 121	sylib	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to \neg (g = j \land h = k \land i = l)$
123		df-ne	$⊢ d \neq j \leftrightarrow \neg d = j$
124		df-ne	$⊢ e \neq k \leftrightarrow \neg e = k$
125		df-ne	$⊢ f \neq l \leftrightarrow \neg f = l$
126	123 124 125	3orbi123i	$⊢ (d \neq j \lor e \neq k \lor f \neq l) \leftrightarrow (\neg d = j \lor \neg e = k \lor \neg f = l)$
127		3ianor	$⊢ \neg (d = j \land e = k \land f = l) \leftrightarrow (\neg d = j \lor \neg e = k \lor \neg f = l)$
128	126 127	bitr4i	$⊢ (d \neq j \lor e \neq k \lor f \neq l) \leftrightarrow \neg (d = j \land e = k \land f = l)$
129	128	con2bii	$⊢ (d = j \land e = k \land f = l) \leftrightarrow \neg (d \neq j \lor e \neq k \lor f \neq l)$
130		breq1	$⊢ d = j \to (d R g \leftrightarrow j R g)$
131		equequ1	$⊢ d = j \to (d = g \leftrightarrow j = g)$
132		equcom	$⊢ j = g \leftrightarrow g = j$
133	131 132	bitrdi	$⊢ d = j \to (d = g \leftrightarrow g = j)$
134	130 133	orbi12d	$⊢ d = j \to ((d R g \lor d = g) \leftrightarrow (j R g \lor g = j))$
135	54 134	syl5ibcom	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (d = j \to (j R g \lor g = j))$
136	135	imp	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land d = j) \to (j R g \lor g = j)$
137	61	adantr	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land d = j) \to (g R j \lor g = j)$
138		ordir	$⊢ ((j R g \land g R j) \lor g = j) \leftrightarrow ((j R g \lor g = j) \land (g R j \lor g = j))$
139	136 137 138	sylanbrc	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land d = j) \to ((j R g \land g R j) \lor g = j)$
140		po2nr	$⊢ (R Po A \land (j \in A \land g \in A)) \to \neg (j R g \land g R j)$
141	38 44 42 140	syl12anc	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to \neg (j R g \land g R j)$
142	141	adantr	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land d = j) \to \neg (j R g \land g R j)$
143	139 142	orcnd	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land d = j) \to g = j$
144	143	ex	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (d = j \to g = j)$
145		breq1	$⊢ e = k \to (e S h \leftrightarrow k S h)$
146		equequ1	$⊢ e = k \to (e = h \leftrightarrow k = h)$
147		equcom	$⊢ k = h \leftrightarrow h = k$
148	146 147	bitrdi	$⊢ e = k \to (e = h \leftrightarrow h = k)$
149	145 148	orbi12d	$⊢ e = k \to ((e S h \lor e = h) \leftrightarrow (k S h \lor h = k))$
150	79 149	syl5ibcom	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (e = k \to (k S h \lor h = k))$
151	150	imp	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land e = k) \to (k S h \lor h = k)$
152	86	adantr	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land e = k) \to (h S k \lor h = k)$
153		ordir	$⊢ ((k S h \land h S k) \lor h = k) \leftrightarrow ((k S h \lor h = k) \land (h S k \lor h = k))$
154	151 152 153	sylanbrc	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land e = k) \to ((k S h \land h S k) \lor h = k)$
155		po2nr	$⊢ (S Po B \land (k \in B \land h \in B)) \to \neg (k S h \land h S k)$
156	63 69 67 155	syl12anc	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to \neg (k S h \land h S k)$
157	156	adantr	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land e = k) \to \neg (k S h \land h S k)$
158	154 157	orcnd	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land e = k) \to h = k$
159	158	ex	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (e = k \to h = k)$
160		breq1	$⊢ f = l \to (f T i \leftrightarrow l T i)$
161		equequ1	$⊢ f = l \to (f = i \leftrightarrow l = i)$
162	160 161	orbi12d	$⊢ f = l \to ((f T i \lor f = i) \leftrightarrow (l T i \lor l = i))$
163	104 162	syl5ibcom	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (f = l \to (l T i \lor l = i))$
164	163	imp	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land f = l) \to (l T i \lor l = i)$
165		equcom	$⊢ l = i \leftrightarrow i = l$
166	165	orbi2i	$⊢ (l T i \lor l = i) \leftrightarrow (l T i \lor i = l)$
167	164 166	sylib	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land f = l) \to (l T i \lor i = l)$
168	111	adantr	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land f = l) \to (i T l \lor i = l)$
169		ordir	$⊢ ((l T i \land i T l) \lor i = l) \leftrightarrow ((l T i \lor i = l) \land (i T l \lor i = l))$
170	167 168 169	sylanbrc	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land f = l) \to ((l T i \land i T l) \lor i = l)$
171		po2nr	$⊢ (T Po C \land (l \in C \land i \in C)) \to \neg (l T i \land i T l)$
172	88 94 92 171	syl12anc	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to \neg (l T i \land i T l)$
173	172	adantr	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land f = l) \to \neg (l T i \land i T l)$
174	170 173	orcnd	$⊢ ((φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \land f = l) \to i = l$
175	174	ex	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (f = l \to i = l)$
176	144 159 175	3anim123d	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to ((d = j \land e = k \land f = l) \to (g = j \land h = k \land i = l))$
177	129 176	syl5bir	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (\neg (d \neq j \lor e \neq k \lor f \neq l) \to (g = j \land h = k \land i = l))$
178	122 177	mt3d	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (d \neq j \lor e \neq k \lor f \neq l)$
179	113 178	jca	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to (((d R j \lor d = j) \land (e S k \lor e = k) \land (f T l \lor f = l)) \land (d \neq j \lor e \neq k \lor f \neq l))$
180	36 37 179	3jca	$⊢ (φ \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))) \to ((d \in A \land e \in B \land f \in C) \land (j \in A \land k \in B \land l \in C) \land (((d R j \lor d = j) \land (e S k \lor e = k) \land (f T l \lor f = l)) \land (d \neq j \lor e \neq k \lor f \neq l)))$
181	180	ex	$⊢ φ \to ((((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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l)))) \to ((d \in A \land e \in B \land f \in C) \land (j \in A \land k \in B \land l \in C) \land (((d R j \lor d = j) \land (e S k \lor e = k) \land (f T l \lor f = l)) \land (d \neq j \lor e \neq k \lor f \neq l))))$
182		breq12	$⊢ (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩) \to (a U b \leftrightarrow ⟨⟨d, e⟩, f⟩ U ⟨⟨g, h⟩, i⟩)$
183	182	3adant3	$⊢ (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to (a U b \leftrightarrow ⟨⟨d, e⟩, f⟩ U ⟨⟨g, h⟩, i⟩)$
184	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)))$
185	183 184	bitrdi	$⊢ (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to (a U b \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))))$
186		breq12	$⊢ (b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to (b U c \leftrightarrow ⟨⟨g, h⟩, i⟩ U ⟨⟨j, k⟩, l⟩)$
187	186	3adant1	$⊢ (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to (b U c \leftrightarrow ⟨⟨g, h⟩, i⟩ U ⟨⟨j, k⟩, l⟩)$
188	1	xpord3lem	$⊢ ⟨⟨g, h⟩, i⟩ U ⟨⟨j, k⟩, l⟩ \leftrightarrow ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l)))$
189	187 188	bitrdi	$⊢ (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to (b U c \leftrightarrow ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l))))$
190	185 189	anbi12d	$⊢ (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to ((a U b \land b U c) \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l)))))$
191		breq12	$⊢ (a = ⟨⟨d, e⟩, f⟩ \land c = ⟨⟨j, k⟩, l⟩) \to (a U c \leftrightarrow ⟨⟨d, e⟩, f⟩ U ⟨⟨j, k⟩, l⟩)$
192	191	3adant2	$⊢ (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to (a U c \leftrightarrow ⟨⟨d, e⟩, f⟩ U ⟨⟨j, k⟩, l⟩)$
193	1	xpord3lem	$⊢ ⟨⟨d, e⟩, f⟩ U ⟨⟨j, k⟩, l⟩ \leftrightarrow ((d \in A \land e \in B \land f \in C) \land (j \in A \land k \in B \land l \in C) \land (((d R j \lor d = j) \land (e S k \lor e = k) \land (f T l \lor f = l)) \land (d \neq j \lor e \neq k \lor f \neq l)))$
194	192 193	bitrdi	$⊢ (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to (a U c \leftrightarrow ((d \in A \land e \in B \land f \in C) \land (j \in A \land k \in B \land l \in C) \land (((d R j \lor d = j) \land (e S k \lor e = k) \land (f T l \lor f = l)) \land (d \neq j \lor e \neq k \lor f \neq l))))$
195	190 194	imbi12d	$⊢ (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to (((a U b \land b U c) \to a U c) \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))) \land ((g \in A \land h \in B \land i \in C) \land (j \in A \land k \in B \land l \in C) \land (((g R j \lor g = j) \land (h S k \lor h = k) \land (i T l \lor i = l)) \land (g \neq j \lor h \neq k \lor i \neq l)))) \to ((d \in A \land e \in B \land f \in C) \land (j \in A \land k \in B \land l \in C) \land (((d R j \lor d = j) \land (e S k \lor e = k) \land (f T l \lor f = l)) \land (d \neq j \lor e \neq k \lor f \neq l)))))$
196	181 195	syl5ibrcom	$⊢ φ \to ((a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to ((a U b \land b U c) \to a U c))$
197	196	rexlimdvw	$⊢ φ \to (\exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to ((a U b \land b U c) \to a U c))$
198	197	a1d	$⊢ φ \to ((f \in C \land i \in C) \to (\exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to ((a U b \land b U c) \to a U c)))$
199	198	rexlimdvv	$⊢ φ \to (\exists f \in C \exists i \in C \exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to ((a U b \land b U c) \to a U c))$
200	199	rexlimdvw	$⊢ φ \to (\exists k \in B \exists f \in C \exists i \in C \exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to ((a U b \land b U c) \to a U c))$
201	200	a1d	$⊢ φ \to ((e \in B \land h \in B) \to (\exists k \in B \exists f \in C \exists i \in C \exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to ((a U b \land b U c) \to a U c)))$
202	201	rexlimdvv	$⊢ φ \to (\exists e \in B \exists h \in B \exists k \in B \exists f \in C \exists i \in C \exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to ((a U b \land b U c) \to a U c))$
203	202	rexlimdvw	$⊢ φ \to (\exists j \in A \exists e \in B \exists h \in B \exists k \in B \exists f \in C \exists i \in C \exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to ((a U b \land b U c) \to a U c))$
204	203	a1d	$⊢ φ \to ((d \in A \land g \in A) \to (\exists j \in A \exists e \in B \exists h \in B \exists k \in B \exists f \in C \exists i \in C \exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to ((a U b \land b U c) \to a U c)))$
205	204	rexlimdvv	$⊢ φ \to (\exists d \in A \exists g \in A \exists j \in A \exists e \in B \exists h \in B \exists k \in B \exists f \in C \exists i \in C \exists l \in C (a = ⟨⟨d, e⟩, f⟩ \land b = ⟨⟨g, h⟩, i⟩ \land c = ⟨⟨j, k⟩, l⟩) \to ((a U b \land b U c) \to a U c))$
206	35 205	syl5bi	$⊢ φ \to ((a \in ((A \times B) \times C) \land b \in ((A \times B) \times C) \land c \in ((A \times B) \times C)) \to ((a U b \land b U c) \to a U c))$
207	206	imp	$⊢ (φ \land (a \in ((A \times B) \times C) \land b \in ((A \times B) \times C) \land c \in ((A \times B) \times C))) \to ((a U b \land b U c) \to a U c)$
208	22 207	ispod	$⊢ φ \to U Po ((A \times B) \times C)$

Metamath Proof Explorer

Theorem poxp3

Proof