frxp3

Description: Give foundedness over a triple cross product. (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))\}$
	frxp3.1	$⊢ φ \to R Fr A$
	frxp3.2	$⊢ φ \to S Fr B$
	frxp3.3	$⊢ φ \to T Fr C$
Assertion	frxp3	$⊢ φ \to U Fr ((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		frxp3.1	$⊢ φ \to R Fr A$
3		frxp3.2	$⊢ φ \to S Fr B$
4		frxp3.3	$⊢ φ \to T Fr C$
5		dmss	$⊢ s \subseteq (A \times B) \times C \to dom s \subseteq dom ((A \times B) \times C)$
6	5	ad2antrl	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to dom s \subseteq dom ((A \times B) \times C)$
7		dmxpss	$⊢ dom ((A \times B) \times C) \subseteq A \times B$
8	6 7	sstrdi	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to dom s \subseteq A \times B$
9		dmss	$⊢ dom s \subseteq A \times B \to dom dom s \subseteq dom (A \times B)$
10	8 9	syl	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to dom dom s \subseteq dom (A \times B)$
11		dmxpss	$⊢ dom (A \times B) \subseteq A$
12	10 11	sstrdi	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to dom dom s \subseteq A$
13		simprr	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to s \neq \emptyset$
14		simprl	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to s \subseteq (A \times B) \times C$
15		relxp	$⊢ Rel ((A \times B) \times C)$
16		relss	$⊢ s \subseteq (A \times B) \times C \to (Rel ((A \times B) \times C) \to Rel s)$
17	14 15 16	mpisyl	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to Rel s$
18		reldm0	$⊢ Rel s \to (s = \emptyset \leftrightarrow dom s = \emptyset)$
19	17 18	syl	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to (s = \emptyset \leftrightarrow dom s = \emptyset)$
20	19	necon3bid	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to (s \neq \emptyset \leftrightarrow dom s \neq \emptyset)$
21	13 20	mpbid	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to dom s \neq \emptyset$
22		relxp	$⊢ Rel (A \times B)$
23		relss	$⊢ dom s \subseteq A \times B \to (Rel (A \times B) \to Rel dom s)$
24	8 22 23	mpisyl	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to Rel dom s$
25		reldm0	$⊢ Rel dom s \to (dom s = \emptyset \leftrightarrow dom dom s = \emptyset)$
26	24 25	syl	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to (dom s = \emptyset \leftrightarrow dom dom s = \emptyset)$
27	26	necon3bid	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to (dom s \neq \emptyset \leftrightarrow dom dom s \neq \emptyset)$
28	21 27	mpbid	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to dom dom s \neq \emptyset$
29		df-fr	$⊢ R Fr A \leftrightarrow \forall g ((g \subseteq A \land g \neq \emptyset) \to \exists a \in g \forall d \in g \neg d R a)$
30	2 29	sylib	$⊢ φ \to \forall g ((g \subseteq A \land g \neq \emptyset) \to \exists a \in g \forall d \in g \neg d R a)$
31	30	adantr	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to \forall g ((g \subseteq A \land g \neq \emptyset) \to \exists a \in g \forall d \in g \neg d R a)$
32		vex	$⊢ s \in V$
33	32	dmex	$⊢ dom s \in V$
34	33	dmex	$⊢ dom dom s \in V$
35		sseq1	$⊢ g = dom dom s \to (g \subseteq A \leftrightarrow dom dom s \subseteq A)$
36		neeq1	$⊢ g = dom dom s \to (g \neq \emptyset \leftrightarrow dom dom s \neq \emptyset)$
37	35 36	anbi12d	$⊢ g = dom dom s \to ((g \subseteq A \land g \neq \emptyset) \leftrightarrow (dom dom s \subseteq A \land dom dom s \neq \emptyset))$
38		raleq	$⊢ g = dom dom s \to (\forall d \in g \neg d R a \leftrightarrow \forall d \in dom dom s \neg d R a)$
39	38	rexeqbi1dv	$⊢ g = dom dom s \to (\exists a \in g \forall d \in g \neg d R a \leftrightarrow \exists a \in dom dom s \forall d \in dom dom s \neg d R a)$
40	37 39	imbi12d	$⊢ g = dom dom s \to (((g \subseteq A \land g \neq \emptyset) \to \exists a \in g \forall d \in g \neg d R a) \leftrightarrow ((dom dom s \subseteq A \land dom dom s \neq \emptyset) \to \exists a \in dom dom s \forall d \in dom dom s \neg d R a))$
41	34 40	spcv	$⊢ \forall g ((g \subseteq A \land g \neq \emptyset) \to \exists a \in g \forall d \in g \neg d R a) \to ((dom dom s \subseteq A \land dom dom s \neq \emptyset) \to \exists a \in dom dom s \forall d \in dom dom s \neg d R a)$
42	31 41	syl	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to ((dom dom s \subseteq A \land dom dom s \neq \emptyset) \to \exists a \in dom dom s \forall d \in dom dom s \neg d R a)$
43	12 28 42	mp2and	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to \exists a \in dom dom s \forall d \in dom dom s \neg d R a$
44		imassrn	$⊢ dom s [\{a\}] \subseteq ran dom s$
45		rnss	$⊢ dom s \subseteq A \times B \to ran dom s \subseteq ran (A \times B)$
46	8 45	syl	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to ran dom s \subseteq ran (A \times B)$
47		rnxpss	$⊢ ran (A \times B) \subseteq B$
48	46 47	sstrdi	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to ran dom s \subseteq B$
49	48	adantr	$⊢ ((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \to ran dom s \subseteq B$
50	44 49	sstrid	$⊢ ((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \to dom s [\{a\}] \subseteq B$
51		simprl	$⊢ ((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \to a \in dom dom s$
52		imadisj	$⊢ dom s [\{a\}] = \emptyset \leftrightarrow dom dom s \cap \{a\} = \emptyset$
53		disjsn	$⊢ dom dom s \cap \{a\} = \emptyset \leftrightarrow \neg a \in dom dom s$
54	52 53	bitri	$⊢ dom s [\{a\}] = \emptyset \leftrightarrow \neg a \in dom dom s$
55	54	necon2abii	$⊢ a \in dom dom s \leftrightarrow dom s [\{a\}] \neq \emptyset$
56	51 55	sylib	$⊢ ((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \to dom s [\{a\}] \neq \emptyset$
57		df-fr	$⊢ S Fr B \leftrightarrow \forall g ((g \subseteq B \land g \neq \emptyset) \to \exists b \in g \forall e \in g \neg e S b)$
58	3 57	sylib	$⊢ φ \to \forall g ((g \subseteq B \land g \neq \emptyset) \to \exists b \in g \forall e \in g \neg e S b)$
59	33	imaex	$⊢ dom s [\{a\}] \in V$
60		sseq1	$⊢ g = dom s [\{a\}] \to (g \subseteq B \leftrightarrow dom s [\{a\}] \subseteq B)$
61		neeq1	$⊢ g = dom s [\{a\}] \to (g \neq \emptyset \leftrightarrow dom s [\{a\}] \neq \emptyset)$
62	60 61	anbi12d	$⊢ g = dom s [\{a\}] \to ((g \subseteq B \land g \neq \emptyset) \leftrightarrow (dom s [\{a\}] \subseteq B \land dom s [\{a\}] \neq \emptyset))$
63		raleq	$⊢ g = dom s [\{a\}] \to (\forall e \in g \neg e S b \leftrightarrow \forall e \in dom s [\{a\}] \neg e S b)$
64	63	rexeqbi1dv	$⊢ g = dom s [\{a\}] \to (\exists b \in g \forall e \in g \neg e S b \leftrightarrow \exists b \in dom s [\{a\}] \forall e \in dom s [\{a\}] \neg e S b)$
65	62 64	imbi12d	$⊢ g = dom s [\{a\}] \to (((g \subseteq B \land g \neq \emptyset) \to \exists b \in g \forall e \in g \neg e S b) \leftrightarrow ((dom s [\{a\}] \subseteq B \land dom s [\{a\}] \neq \emptyset) \to \exists b \in dom s [\{a\}] \forall e \in dom s [\{a\}] \neg e S b))$
66	59 65	spcv	$⊢ \forall g ((g \subseteq B \land g \neq \emptyset) \to \exists b \in g \forall e \in g \neg e S b) \to ((dom s [\{a\}] \subseteq B \land dom s [\{a\}] \neq \emptyset) \to \exists b \in dom s [\{a\}] \forall e \in dom s [\{a\}] \neg e S b)$
67	58 66	syl	$⊢ φ \to ((dom s [\{a\}] \subseteq B \land dom s [\{a\}] \neq \emptyset) \to \exists b \in dom s [\{a\}] \forall e \in dom s [\{a\}] \neg e S b)$
68	67	ad2antrr	$⊢ ((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \to ((dom s [\{a\}] \subseteq B \land dom s [\{a\}] \neq \emptyset) \to \exists b \in dom s [\{a\}] \forall e \in dom s [\{a\}] \neg e S b)$
69	50 56 68	mp2and	$⊢ ((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \to \exists b \in dom s [\{a\}] \forall e \in dom s [\{a\}] \neg e S b$
70		imassrn	$⊢ s [\{⟨a, b⟩\}] \subseteq ran s$
71		rnss	$⊢ s \subseteq (A \times B) \times C \to ran s \subseteq ran ((A \times B) \times C)$
72	71	ad2antrl	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to ran s \subseteq ran ((A \times B) \times C)$
73		rnxpss	$⊢ ran ((A \times B) \times C) \subseteq C$
74	72 73	sstrdi	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to ran s \subseteq C$
75	70 74	sstrid	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to s [\{⟨a, b⟩\}] \subseteq C$
76	75	ad2antrr	$⊢ (((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \to s [\{⟨a, b⟩\}] \subseteq C$
77		simprl	$⊢ (((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \to b \in dom s [\{a\}]$
78		vex	$⊢ a \in V$
79		vex	$⊢ b \in V$
80	78 79	elimasn	$⊢ b \in dom s [\{a\}] \leftrightarrow ⟨a, b⟩ \in dom s$
81	77 80	sylib	$⊢ (((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \to ⟨a, b⟩ \in dom s$
82		imadisj	$⊢ s [\{⟨a, b⟩\}] = \emptyset \leftrightarrow dom s \cap \{⟨a, b⟩\} = \emptyset$
83		disjsn	$⊢ dom s \cap \{⟨a, b⟩\} = \emptyset \leftrightarrow \neg ⟨a, b⟩ \in dom s$
84	82 83	bitri	$⊢ s [\{⟨a, b⟩\}] = \emptyset \leftrightarrow \neg ⟨a, b⟩ \in dom s$
85	84	necon2abii	$⊢ ⟨a, b⟩ \in dom s \leftrightarrow s [\{⟨a, b⟩\}] \neq \emptyset$
86	81 85	sylib	$⊢ (((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \to s [\{⟨a, b⟩\}] \neq \emptyset$
87		df-fr	$⊢ T Fr C \leftrightarrow \forall g ((g \subseteq C \land g \neq \emptyset) \to \exists c \in g \forall f \in g \neg f T c)$
88	4 87	sylib	$⊢ φ \to \forall g ((g \subseteq C \land g \neq \emptyset) \to \exists c \in g \forall f \in g \neg f T c)$
89	32	imaex	$⊢ s [\{⟨a, b⟩\}] \in V$
90		sseq1	$⊢ g = s [\{⟨a, b⟩\}] \to (g \subseteq C \leftrightarrow s [\{⟨a, b⟩\}] \subseteq C)$
91		neeq1	$⊢ g = s [\{⟨a, b⟩\}] \to (g \neq \emptyset \leftrightarrow s [\{⟨a, b⟩\}] \neq \emptyset)$
92	90 91	anbi12d	$⊢ g = s [\{⟨a, b⟩\}] \to ((g \subseteq C \land g \neq \emptyset) \leftrightarrow (s [\{⟨a, b⟩\}] \subseteq C \land s [\{⟨a, b⟩\}] \neq \emptyset))$
93		raleq	$⊢ g = s [\{⟨a, b⟩\}] \to (\forall f \in g \neg f T c \leftrightarrow \forall f \in s [\{⟨a, b⟩\}] \neg f T c)$
94	93	rexeqbi1dv	$⊢ g = s [\{⟨a, b⟩\}] \to (\exists c \in g \forall f \in g \neg f T c \leftrightarrow \exists c \in s [\{⟨a, b⟩\}] \forall f \in s [\{⟨a, b⟩\}] \neg f T c)$
95	92 94	imbi12d	$⊢ g = s [\{⟨a, b⟩\}] \to (((g \subseteq C \land g \neq \emptyset) \to \exists c \in g \forall f \in g \neg f T c) \leftrightarrow ((s [\{⟨a, b⟩\}] \subseteq C \land s [\{⟨a, b⟩\}] \neq \emptyset) \to \exists c \in s [\{⟨a, b⟩\}] \forall f \in s [\{⟨a, b⟩\}] \neg f T c))$
96	89 95	spcv	$⊢ \forall g ((g \subseteq C \land g \neq \emptyset) \to \exists c \in g \forall f \in g \neg f T c) \to ((s [\{⟨a, b⟩\}] \subseteq C \land s [\{⟨a, b⟩\}] \neq \emptyset) \to \exists c \in s [\{⟨a, b⟩\}] \forall f \in s [\{⟨a, b⟩\}] \neg f T c)$
97	88 96	syl	$⊢ φ \to ((s [\{⟨a, b⟩\}] \subseteq C \land s [\{⟨a, b⟩\}] \neq \emptyset) \to \exists c \in s [\{⟨a, b⟩\}] \forall f \in s [\{⟨a, b⟩\}] \neg f T c)$
98	97	ad3antrrr	$⊢ (((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \to ((s [\{⟨a, b⟩\}] \subseteq C \land s [\{⟨a, b⟩\}] \neq \emptyset) \to \exists c \in s [\{⟨a, b⟩\}] \forall f \in s [\{⟨a, b⟩\}] \neg f T c)$
99	76 86 98	mp2and	$⊢ (((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \to \exists c \in s [\{⟨a, b⟩\}] \forall f \in s [\{⟨a, b⟩\}] \neg f T c$
100		simprl	$⊢ ((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \to c \in s [\{⟨a, b⟩\}]$
101		opex	$⊢ ⟨a, b⟩ \in V$
102		vex	$⊢ c \in V$
103	101 102	elimasn	$⊢ c \in s [\{⟨a, b⟩\}] \leftrightarrow ⟨⟨a, b⟩, c⟩ \in s$
104	100 103	sylib	$⊢ ((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \to ⟨⟨a, b⟩, c⟩ \in s$
105		simplrl	$⊢ ((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \to s \subseteq (A \times B) \times C$
106	105	ad2antrr	$⊢ ((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \to s \subseteq (A \times B) \times C$
107		elxpxpss	$⊢ (s \subseteq (A \times B) \times C \land q \in s) \to \exists g \exists h \exists i q = ⟨⟨g, h⟩, i⟩$
108	106 107	sylan	$⊢ (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land q \in s) \to \exists g \exists h \exists i q = ⟨⟨g, h⟩, i⟩$
109		df-ne	$⊢ i \neq c \leftrightarrow \neg i = c$
110	109	con2bii	$⊢ i = c \leftrightarrow \neg i \neq c$
111	110	biimpi	$⊢ i = c \to \neg i \neq c$
112	111	adantl	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, b⟩, i⟩ \in s) \land i = c) \to \neg i \neq c$
113	112	intnand	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, b⟩, i⟩ \in s) \land i = c) \to \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land i \neq c)$
114		breq1	$⊢ f = i \to (f T c \leftrightarrow i T c)$
115	114	notbid	$⊢ f = i \to (\neg f T c \leftrightarrow \neg i T c)$
116		simplrr	$⊢ (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, b⟩, i⟩ \in s) \to \forall f \in s [\{⟨a, b⟩\}] \neg f T c$
117	116	adantr	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, b⟩, i⟩ \in s) \land i \neq c) \to \forall f \in s [\{⟨a, b⟩\}] \neg f T c$
118		simplr	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, b⟩, i⟩ \in s) \land i \neq c) \to ⟨⟨a, b⟩, i⟩ \in s$
119		vex	$⊢ i \in V$
120	101 119	elimasn	$⊢ i \in s [\{⟨a, b⟩\}] \leftrightarrow ⟨⟨a, b⟩, i⟩ \in s$
121	118 120	sylibr	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, b⟩, i⟩ \in s) \land i \neq c) \to i \in s [\{⟨a, b⟩\}]$
122	115 117 121	rspcdva	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, b⟩, i⟩ \in s) \land i \neq c) \to \neg i T c$
123		simpr	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, b⟩, i⟩ \in s) \land i \neq c) \to i \neq c$
124	123	neneqd	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, b⟩, i⟩ \in s) \land i \neq c) \to \neg i = c$
125		ioran	$⊢ \neg (i T c \lor i = c) \leftrightarrow (\neg i T c \land \neg i = c)$
126	122 124 125	sylanbrc	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, b⟩, i⟩ \in s) \land i \neq c) \to \neg (i T c \lor i = c)$
127	126	intn3an3d	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, b⟩, i⟩ \in s) \land i \neq c) \to \neg ((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c))$
128	127	intnanrd	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, b⟩, i⟩ \in s) \land i \neq c) \to \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land i \neq c)$
129	113 128	pm2.61dane	$⊢ (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, b⟩, i⟩ \in s) \to \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land i \neq c)$
130		opeq2	$⊢ h = b \to ⟨a, h⟩ = ⟨a, b⟩$
131	130	opeq1d	$⊢ h = b \to ⟨⟨a, h⟩, i⟩ = ⟨⟨a, b⟩, i⟩$
132	131	eleq1d	$⊢ h = b \to (⟨⟨a, h⟩, i⟩ \in s \leftrightarrow ⟨⟨a, b⟩, i⟩ \in s)$
133	132	anbi2d	$⊢ h = b \to ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \leftrightarrow (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, b⟩, i⟩ \in s))$
134		neeq1	$⊢ h = b \to (h \neq b \leftrightarrow b \neq b)$
135	134	orbi1d	$⊢ h = b \to ((h \neq b \lor i \neq c) \leftrightarrow (b \neq b \lor i \neq c))$
136		neirr	$⊢ \neg b \neq b$
137		orel1	$⊢ \neg b \neq b \to ((b \neq b \lor i \neq c) \to i \neq c)$
138	136 137	ax-mp	$⊢ (b \neq b \lor i \neq c) \to i \neq c$
139		olc	$⊢ i \neq c \to (b \neq b \lor i \neq c)$
140	138 139	impbii	$⊢ (b \neq b \lor i \neq c) \leftrightarrow i \neq c$
141	135 140	bitrdi	$⊢ h = b \to ((h \neq b \lor i \neq c) \leftrightarrow i \neq c)$
142	141	anbi2d	$⊢ h = b \to ((((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (h \neq b \lor i \neq c)) \leftrightarrow (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land i \neq c))$
143	142	notbid	$⊢ h = b \to (\neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (h \neq b \lor i \neq c)) \leftrightarrow \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land i \neq c))$
144	133 143	imbi12d	$⊢ h = b \to (((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \to \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (h \neq b \lor i \neq c))) \leftrightarrow ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, b⟩, i⟩ \in s) \to \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land i \neq c)))$
145	129 144	mpbiri	$⊢ h = b \to ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \to \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (h \neq b \lor i \neq c)))$
146	145	impcom	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \land h = b) \to \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (h \neq b \lor i \neq c))$
147		breq1	$⊢ e = h \to (e S b \leftrightarrow h S b)$
148	147	notbid	$⊢ e = h \to (\neg e S b \leftrightarrow \neg h S b)$
149		simplrr	$⊢ ((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \to \forall e \in dom s [\{a\}] \neg e S b$
150	149	ad2antrr	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \land h \neq b) \to \forall e \in dom s [\{a\}] \neg e S b$
151		opex	$⊢ ⟨a, h⟩ \in V$
152	151 119	opeldm	$⊢ ⟨⟨a, h⟩, i⟩ \in s \to ⟨a, h⟩ \in dom s$
153	152	adantl	$⊢ (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \to ⟨a, h⟩ \in dom s$
154	153	adantr	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \land h \neq b) \to ⟨a, h⟩ \in dom s$
155		vex	$⊢ h \in V$
156	78 155	elimasn	$⊢ h \in dom s [\{a\}] \leftrightarrow ⟨a, h⟩ \in dom s$
157	154 156	sylibr	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \land h \neq b) \to h \in dom s [\{a\}]$
158	148 150 157	rspcdva	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \land h \neq b) \to \neg h S b$
159		simpr	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \land h \neq b) \to h \neq b$
160	159	neneqd	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \land h \neq b) \to \neg h = b$
161		ioran	$⊢ \neg (h S b \lor h = b) \leftrightarrow (\neg h S b \land \neg h = b)$
162	158 160 161	sylanbrc	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \land h \neq b) \to \neg (h S b \lor h = b)$
163	162	intn3an2d	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \land h \neq b) \to \neg ((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c))$
164	163	intnanrd	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \land h \neq b) \to \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (h \neq b \lor i \neq c))$
165	146 164	pm2.61dane	$⊢ (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \to \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (h \neq b \lor i \neq c))$
166		opeq1	$⊢ g = a \to ⟨g, h⟩ = ⟨a, h⟩$
167	166	opeq1d	$⊢ g = a \to ⟨⟨g, h⟩, i⟩ = ⟨⟨a, h⟩, i⟩$
168	167	eleq1d	$⊢ g = a \to (⟨⟨g, h⟩, i⟩ \in s \leftrightarrow ⟨⟨a, h⟩, i⟩ \in s)$
169	168	anbi2d	$⊢ g = a \to ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \leftrightarrow (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s))$
170		3orass	$⊢ (g \neq a \lor h \neq b \lor i \neq c) \leftrightarrow (g \neq a \lor (h \neq b \lor i \neq c))$
171		neeq1	$⊢ g = a \to (g \neq a \leftrightarrow a \neq a)$
172	171	orbi1d	$⊢ g = a \to ((g \neq a \lor (h \neq b \lor i \neq c)) \leftrightarrow (a \neq a \lor (h \neq b \lor i \neq c)))$
173	170 172	syl5bb	$⊢ g = a \to ((g \neq a \lor h \neq b \lor i \neq c) \leftrightarrow (a \neq a \lor (h \neq b \lor i \neq c)))$
174		neirr	$⊢ \neg a \neq a$
175		orel1	$⊢ \neg a \neq a \to ((a \neq a \lor (h \neq b \lor i \neq c)) \to (h \neq b \lor i \neq c))$
176	174 175	ax-mp	$⊢ (a \neq a \lor (h \neq b \lor i \neq c)) \to (h \neq b \lor i \neq c)$
177		olc	$⊢ (h \neq b \lor i \neq c) \to (a \neq a \lor (h \neq b \lor i \neq c))$
178	176 177	impbii	$⊢ (a \neq a \lor (h \neq b \lor i \neq c)) \leftrightarrow (h \neq b \lor i \neq c)$
179	173 178	bitrdi	$⊢ g = a \to ((g \neq a \lor h \neq b \lor i \neq c) \leftrightarrow (h \neq b \lor i \neq c))$
180	179	anbi2d	$⊢ g = a \to ((((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (g \neq a \lor h \neq b \lor i \neq c)) \leftrightarrow (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (h \neq b \lor i \neq c)))$
181	180	notbid	$⊢ g = a \to (\neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (g \neq a \lor h \neq b \lor i \neq c)) \leftrightarrow \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (h \neq b \lor i \neq c)))$
182	169 181	imbi12d	$⊢ g = a \to (((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \to \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (g \neq a \lor h \neq b \lor i \neq c))) \leftrightarrow ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨a, h⟩, i⟩ \in s) \to \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (h \neq b \lor i \neq c))))$
183	165 182	mpbiri	$⊢ g = a \to ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \to \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (g \neq a \lor h \neq b \lor i \neq c)))$
184	183	impcom	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \land g = a) \to \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (g \neq a \lor h \neq b \lor i \neq c))$
185		breq1	$⊢ d = g \to (d R a \leftrightarrow g R a)$
186	185	notbid	$⊢ d = g \to (\neg d R a \leftrightarrow \neg g R a)$
187		simplrr	$⊢ (((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \to \forall d \in dom dom s \neg d R a$
188	187	ad3antrrr	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \land g \neq a) \to \forall d \in dom dom s \neg d R a$
189		opex	$⊢ ⟨g, h⟩ \in V$
190	189 119	opeldm	$⊢ ⟨⟨g, h⟩, i⟩ \in s \to ⟨g, h⟩ \in dom s$
191	190	adantl	$⊢ (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \to ⟨g, h⟩ \in dom s$
192		vex	$⊢ g \in V$
193	192 155	opeldm	$⊢ ⟨g, h⟩ \in dom s \to g \in dom dom s$
194	191 193	syl	$⊢ (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \to g \in dom dom s$
195	194	adantr	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \land g \neq a) \to g \in dom dom s$
196	186 188 195	rspcdva	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \land g \neq a) \to \neg g R a$
197		simpr	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \land g \neq a) \to g \neq a$
198	197	neneqd	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \land g \neq a) \to \neg g = a$
199		ioran	$⊢ \neg (g R a \lor g = a) \leftrightarrow (\neg g R a \land \neg g = a)$
200	196 198 199	sylanbrc	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \land g \neq a) \to \neg (g R a \lor g = a)$
201	200	intn3an1d	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \land g \neq a) \to \neg ((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c))$
202	201	intnanrd	$⊢ ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \land g \neq a) \to \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (g \neq a \lor h \neq b \lor i \neq c))$
203	184 202	pm2.61dane	$⊢ (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \to \neg (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (g \neq a \lor h \neq b \lor i \neq c))$
204	203	intn3an3d	$⊢ (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \to \neg ((g \in A \land h \in B \land i \in C) \land (a \in A \land b \in B \land c \in C) \land (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (g \neq a \lor h \neq b \lor i \neq c)))$
205		eleq1	$⊢ q = ⟨⟨g, h⟩, i⟩ \to (q \in s \leftrightarrow ⟨⟨g, h⟩, i⟩ \in s)$
206	205	anbi2d	$⊢ q = ⟨⟨g, h⟩, i⟩ \to ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land q \in s) \leftrightarrow (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s))$
207		breq1	$⊢ q = ⟨⟨g, h⟩, i⟩ \to (q U ⟨⟨a, b⟩, c⟩ \leftrightarrow ⟨⟨g, h⟩, i⟩ U ⟨⟨a, b⟩, c⟩)$
208	1	xpord3lem	$⊢ ⟨⟨g, h⟩, i⟩ U ⟨⟨a, b⟩, c⟩ \leftrightarrow ((g \in A \land h \in B \land i \in C) \land (a \in A \land b \in B \land c \in C) \land (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (g \neq a \lor h \neq b \lor i \neq c)))$
209	207 208	bitrdi	$⊢ q = ⟨⟨g, h⟩, i⟩ \to (q U ⟨⟨a, b⟩, c⟩ \leftrightarrow ((g \in A \land h \in B \land i \in C) \land (a \in A \land b \in B \land c \in C) \land (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (g \neq a \lor h \neq b \lor i \neq c))))$
210	209	notbid	$⊢ q = ⟨⟨g, h⟩, i⟩ \to (\neg q U ⟨⟨a, b⟩, c⟩ \leftrightarrow \neg ((g \in A \land h \in B \land i \in C) \land (a \in A \land b \in B \land c \in C) \land (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (g \neq a \lor h \neq b \lor i \neq c))))$
211	206 210	imbi12d	$⊢ q = ⟨⟨g, h⟩, i⟩ \to (((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land q \in s) \to \neg q U ⟨⟨a, b⟩, c⟩) \leftrightarrow ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land ⟨⟨g, h⟩, i⟩ \in s) \to \neg ((g \in A \land h \in B \land i \in C) \land (a \in A \land b \in B \land c \in C) \land (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land (g \neq a \lor h \neq b \lor i \neq c)))))$
212	204 211	mpbiri	$⊢ q = ⟨⟨g, h⟩, i⟩ \to ((((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land q \in s) \to \neg q U ⟨⟨a, b⟩, c⟩)$
213	212	com12	$⊢ (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land q \in s) \to (q = ⟨⟨g, h⟩, i⟩ \to \neg q U ⟨⟨a, b⟩, c⟩)$
214	213	exlimdv	$⊢ (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land q \in s) \to (\exists i q = ⟨⟨g, h⟩, i⟩ \to \neg q U ⟨⟨a, b⟩, c⟩)$
215	214	exlimdvv	$⊢ (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land q \in s) \to (\exists g \exists h \exists i q = ⟨⟨g, h⟩, i⟩ \to \neg q U ⟨⟨a, b⟩, c⟩)$
216	108 215	mpd	$⊢ (((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \land q \in s) \to \neg q U ⟨⟨a, b⟩, c⟩$
217	216	ralrimiva	$⊢ ((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \to \forall q \in s \neg q U ⟨⟨a, b⟩, c⟩$
218		breq2	$⊢ p = ⟨⟨a, b⟩, c⟩ \to (q U p \leftrightarrow q U ⟨⟨a, b⟩, c⟩)$
219	218	notbid	$⊢ p = ⟨⟨a, b⟩, c⟩ \to (\neg q U p \leftrightarrow \neg q U ⟨⟨a, b⟩, c⟩)$
220	219	ralbidv	$⊢ p = ⟨⟨a, b⟩, c⟩ \to (\forall q \in s \neg q U p \leftrightarrow \forall q \in s \neg q U ⟨⟨a, b⟩, c⟩)$
221	220	rspcev	$⊢ (⟨⟨a, b⟩, c⟩ \in s \land \forall q \in s \neg q U ⟨⟨a, b⟩, c⟩) \to \exists p \in s \forall q \in s \neg q U p$
222	104 217 221	syl2anc	$⊢ ((((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \land (c \in s [\{⟨a, b⟩\}] \land \forall f \in s [\{⟨a, b⟩\}] \neg f T c)) \to \exists p \in s \forall q \in s \neg q U p$
223	99 222	rexlimddv	$⊢ (((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \land (b \in dom s [\{a\}] \land \forall e \in dom s [\{a\}] \neg e S b)) \to \exists p \in s \forall q \in s \neg q U p$
224	69 223	rexlimddv	$⊢ ((φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \land (a \in dom dom s \land \forall d \in dom dom s \neg d R a)) \to \exists p \in s \forall q \in s \neg q U p$
225	43 224	rexlimddv	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to \exists p \in s \forall q \in s \neg q U p$
226	225	ex	$⊢ φ \to ((s \subseteq (A \times B) \times C \land s \neq \emptyset) \to \exists p \in s \forall q \in s \neg q U p)$
227	226	alrimiv	$⊢ φ \to \forall s ((s \subseteq (A \times B) \times C \land s \neq \emptyset) \to \exists p \in s \forall q \in s \neg q U p)$
228		df-fr	$⊢ U Fr ((A \times B) \times C) \leftrightarrow \forall s ((s \subseteq (A \times B) \times C \land s \neq \emptyset) \to \exists p \in s \forall q \in s \neg q U p)$
229	227 228	sylibr	$⊢ φ \to U Fr ((A \times B) \times C)$

Metamath Proof Explorer

Theorem frxp3

Proof