frxp3

Description: Give well-foundedness over a triple Cartesian 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	2	adantr	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to R Fr A$
6		dmss	$⊢ s \subseteq (A \times B) \times C \to dom s \subseteq dom ((A \times B) \times C)$
7	6	ad2antrl	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to dom s \subseteq dom ((A \times B) \times C)$
8		dmxpss	$⊢ dom ((A \times B) \times C) \subseteq A \times B$
9	7 8	sstrdi	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to dom s \subseteq A \times B$
10		dmss	$⊢ dom s \subseteq A \times B \to dom dom s \subseteq dom (A \times B)$
11	9 10	syl	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to dom dom s \subseteq dom (A \times B)$
12		dmxpss	$⊢ dom (A \times B) \subseteq A$
13	11 12	sstrdi	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to dom dom s \subseteq A$
14		vex	$⊢ s \in V$
15	14	dmex	$⊢ dom s \in V$
16	15	dmex	$⊢ dom dom s \in V$
17	16	a1i	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to dom dom s \in V$
18		relxp	$⊢ Rel ((A \times B) \times C)$
19		relss	$⊢ s \subseteq (A \times B) \times C \to (Rel ((A \times B) \times C) \to Rel s)$
20	18 19	mpi	$⊢ s \subseteq (A \times B) \times C \to Rel s$
21	20	adantl	$⊢ (φ \land s \subseteq (A \times B) \times C) \to Rel s$
22		reldm0	$⊢ Rel s \to (s = \emptyset \leftrightarrow dom s = \emptyset)$
23	21 22	syl	$⊢ (φ \land s \subseteq (A \times B) \times C) \to (s = \emptyset \leftrightarrow dom s = \emptyset)$
24		relxp	$⊢ Rel (A \times B)$
25		relss	$⊢ dom ((A \times B) \times C) \subseteq A \times B \to (Rel (A \times B) \to Rel dom ((A \times B) \times C))$
26	8 24 25	mp2	$⊢ Rel dom ((A \times B) \times C)$
27		relss	$⊢ dom s \subseteq dom ((A \times B) \times C) \to (Rel dom ((A \times B) \times C) \to Rel dom s)$
28	6 26 27	mpisyl	$⊢ s \subseteq (A \times B) \times C \to Rel dom s$
29	28	adantl	$⊢ (φ \land s \subseteq (A \times B) \times C) \to Rel dom s$
30		reldm0	$⊢ Rel dom s \to (dom s = \emptyset \leftrightarrow dom dom s = \emptyset)$
31	29 30	syl	$⊢ (φ \land s \subseteq (A \times B) \times C) \to (dom s = \emptyset \leftrightarrow dom dom s = \emptyset)$
32	23 31	bitrd	$⊢ (φ \land s \subseteq (A \times B) \times C) \to (s = \emptyset \leftrightarrow dom dom s = \emptyset)$
33	32	necon3bid	$⊢ (φ \land s \subseteq (A \times B) \times C) \to (s \neq \emptyset \leftrightarrow dom dom s \neq \emptyset)$
34	33	biimpa	$⊢ ((φ \land s \subseteq (A \times B) \times C) \land s \neq \emptyset) \to dom dom s \neq \emptyset$
35	34	anasss	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to dom dom s \neq \emptyset$
36	5 13 17 35	frd	$⊢ (φ \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$
37	3	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 S Fr B$
38		imassrn	$⊢ dom s [\{a\}] \subseteq ran dom s$
39		rnss	$⊢ dom s \subseteq A \times B \to ran dom s \subseteq ran (A \times B)$
40	9 39	syl	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to ran dom s \subseteq ran (A \times B)$
41		rnxpss	$⊢ ran (A \times B) \subseteq B$
42	40 41	sstrdi	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to ran dom s \subseteq B$
43	38 42	sstrid	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to dom s [\{a\}] \subseteq B$
44	43	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 dom s [\{a\}] \subseteq B$
45	15	imaex	$⊢ dom s [\{a\}] \in V$
46	45	a1i	$⊢ ((φ \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\}] \in V$
47		imadisj	$⊢ dom s [\{a\}] = \emptyset \leftrightarrow dom dom s \cap \{a\} = \emptyset$
48		disjsn	$⊢ dom dom s \cap \{a\} = \emptyset \leftrightarrow \neg a \in dom dom s$
49	47 48	bitri	$⊢ dom s [\{a\}] = \emptyset \leftrightarrow \neg a \in dom dom s$
50	49	necon2abii	$⊢ a \in dom dom s \leftrightarrow dom s [\{a\}] \neq \emptyset$
51	50	biimpi	$⊢ a \in dom dom s \to dom s [\{a\}] \neq \emptyset$
52	51	ad2antrl	$⊢ ((φ \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$
53	37 44 46 52	frd	$⊢ ((φ \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$
54	4	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 T Fr C$
55		imassrn	$⊢ s [\{⟨a, b⟩\}] \subseteq ran s$
56		rnss	$⊢ s \subseteq (A \times B) \times C \to ran s \subseteq ran ((A \times B) \times C)$
57	56	ad2antrl	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to ran s \subseteq ran ((A \times B) \times C)$
58		rnxpss	$⊢ ran ((A \times B) \times C) \subseteq C$
59	57 58	sstrdi	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to ran s \subseteq C$
60	55 59	sstrid	$⊢ (φ \land (s \subseteq (A \times B) \times C \land s \neq \emptyset)) \to s [\{⟨a, b⟩\}] \subseteq C$
61	60	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$
62	14	imaex	$⊢ s [\{⟨a, b⟩\}] \in V$
63	62	a1i	$⊢ (((φ \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⟩\}] \in V$
64		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\}]$
65		vex	$⊢ a \in V$
66		vex	$⊢ b \in V$
67	65 66	elimasn	$⊢ b \in dom s [\{a\}] \leftrightarrow ⟨a, b⟩ \in dom s$
68	64 67	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$
69		imadisj	$⊢ s [\{⟨a, b⟩\}] = \emptyset \leftrightarrow dom s \cap \{⟨a, b⟩\} = \emptyset$
70		disjsn	$⊢ dom s \cap \{⟨a, b⟩\} = \emptyset \leftrightarrow \neg ⟨a, b⟩ \in dom s$
71	69 70	bitri	$⊢ s [\{⟨a, b⟩\}] = \emptyset \leftrightarrow \neg ⟨a, b⟩ \in dom s$
72	71	necon2abii	$⊢ ⟨a, b⟩ \in dom s \leftrightarrow s [\{⟨a, b⟩\}] \neq \emptyset$
73	68 72	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$
74	54 61 63 73	frd	$⊢ (((φ \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$
75		df-ot	$⊢ ⟨a, b, c⟩ = ⟨⟨a, b⟩, c⟩$
76		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⟩\}]$
77		opex	$⊢ ⟨a, b⟩ \in V$
78		vex	$⊢ c \in V$
79	77 78	elimasn	$⊢ c \in s [\{⟨a, b⟩\}] \leftrightarrow ⟨⟨a, b⟩, c⟩ \in s$
80	76 79	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$
81	75 80	eqeltrid	$⊢ ((((φ \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$
82		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$
83	82	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$
84		el2xpss	$⊢ (q \in s \land s \subseteq (A \times B) \times C) \to \exists g \exists h \exists i q = ⟨g, h, i⟩$
85	84	ancoms	$⊢ (s \subseteq (A \times B) \times C \land q \in s) \to \exists g \exists h \exists i q = ⟨g, h, i⟩$
86	83 85	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⟩$
87		df-ne	$⊢ i \neq c \leftrightarrow \neg i = c$
88	87	con2bii	$⊢ i = c \leftrightarrow \neg i \neq c$
89	88	biimpi	$⊢ i = c \to \neg i \neq c$
90	89	intnand	$⊢ 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)$
91	90	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 (((g R a \lor g = a) \land (h S b \lor h = b) \land (i T c \lor i = c)) \land i \neq c)$
92		breq1	$⊢ f = i \to (f T c \leftrightarrow i T c)$
93	92	notbid	$⊢ f = i \to (\neg f T c \leftrightarrow \neg i T c)$
94		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$
95	94	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$
96		df-ot	$⊢ ⟨a, b, i⟩ = ⟨⟨a, b⟩, i⟩$
97		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$
98	96 97	eqeltrrid	$⊢ ((((((φ \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$
99		vex	$⊢ i \in V$
100	77 99	elimasn	$⊢ i \in s [\{⟨a, b⟩\}] \leftrightarrow ⟨⟨a, b⟩, i⟩ \in s$
101	98 100	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⟩\}]$
102	93 95 101	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$
103		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$
104	103	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$
105		ioran	$⊢ \neg (i T c \lor i = c) \leftrightarrow (\neg i T c \land \neg i = c)$
106	102 104 105	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)$
107	106	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))$
108	107	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)$
109	91 108	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)$
110		oteq2	$⊢ h = b \to ⟨a, h, i⟩ = ⟨a, b, i⟩$
111	110	eleq1d	$⊢ h = b \to (⟨a, h, i⟩ \in s \leftrightarrow ⟨a, b, i⟩ \in s)$
112	111	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))$
113		neeq1	$⊢ h = b \to (h \neq b \leftrightarrow b \neq b)$
114	113	orbi1d	$⊢ h = b \to ((h \neq b \lor i \neq c) \leftrightarrow (b \neq b \lor i \neq c))$
115		neirr	$⊢ \neg b \neq b$
116		orel1	$⊢ \neg b \neq b \to ((b \neq b \lor i \neq c) \to i \neq c)$
117	115 116	ax-mp	$⊢ (b \neq b \lor i \neq c) \to i \neq c$
118		olc	$⊢ i \neq c \to (b \neq b \lor i \neq c)$
119	117 118	impbii	$⊢ (b \neq b \lor i \neq c) \leftrightarrow i \neq c$
120	114 119	bitrdi	$⊢ h = b \to ((h \neq b \lor i \neq c) \leftrightarrow i \neq c)$
121	120	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))$
122	121	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))$
123	112 122	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)))$
124	109 123	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)))$
125	124	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))$
126		breq1	$⊢ e = h \to (e S b \leftrightarrow h S b)$
127	126	notbid	$⊢ e = h \to (\neg e S b \leftrightarrow \neg h S b)$
128		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$
129	128	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$
130		df-ot	$⊢ ⟨a, h, i⟩ = ⟨⟨a, h⟩, i⟩$
131		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, h, i⟩ \in s) \land h \neq b) \to ⟨a, h, i⟩ \in s$
132	130 131	eqeltrrid	$⊢ ((((((φ \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⟩, i⟩ \in s$
133		opex	$⊢ ⟨a, h⟩ \in V$
134	133 99	opeldm	$⊢ ⟨⟨a, h⟩, i⟩ \in s \to ⟨a, h⟩ \in dom s$
135	132 134	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 ⟨a, h, i⟩ \in s) \land h \neq b) \to ⟨a, h⟩ \in dom s$
136		vex	$⊢ h \in V$
137	65 136	elimasn	$⊢ h \in dom s [\{a\}] \leftrightarrow ⟨a, h⟩ \in dom s$
138	135 137	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\}]$
139	127 129 138	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$
140		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$
141	140	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$
142		ioran	$⊢ \neg (h S b \lor h = b) \leftrightarrow (\neg h S b \land \neg h = b)$
143	139 141 142	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)$
144	143	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))$
145	144	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))$
146	125 145	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))$
147		oteq1	$⊢ g = a \to ⟨g, h, i⟩ = ⟨a, h, i⟩$
148	147	eleq1d	$⊢ g = a \to (⟨g, h, i⟩ \in s \leftrightarrow ⟨a, h, i⟩ \in s)$
149	148	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))$
150		neeq1	$⊢ g = a \to (g \neq a \leftrightarrow a \neq a)$
151		biidd	$⊢ g = a \to (h \neq b \leftrightarrow h \neq b)$
152		biidd	$⊢ g = a \to (i \neq c \leftrightarrow i \neq c)$
153	150 151 152	3orbi123d	$⊢ 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))$
154		3orass	$⊢ (a \neq a \lor h \neq b \lor i \neq c) \leftrightarrow (a \neq a \lor (h \neq b \lor i \neq c))$
155		neirr	$⊢ \neg a \neq a$
156		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))$
157	155 156	ax-mp	$⊢ (a \neq a \lor (h \neq b \lor i \neq c)) \to (h \neq b \lor i \neq c)$
158		olc	$⊢ (h \neq b \lor i \neq c) \to (a \neq a \lor (h \neq b \lor i \neq c))$
159	157 158	impbii	$⊢ (a \neq a \lor (h \neq b \lor i \neq c)) \leftrightarrow (h \neq b \lor i \neq c)$
160	154 159	bitri	$⊢ (a \neq a \lor h \neq b \lor i \neq c) \leftrightarrow (h \neq b \lor i \neq c)$
161	153 160	bitrdi	$⊢ g = a \to ((g \neq a \lor h \neq b \lor i \neq c) \leftrightarrow (h \neq b \lor i \neq c))$
162	161	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)))$
163	162	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)))$
164	149 163	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))))$
165	146 164	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)))$
166	165	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))$
167		breq1	$⊢ d = g \to (d R a \leftrightarrow g R a)$
168	167	notbid	$⊢ d = g \to (\neg d R a \leftrightarrow \neg g R a)$
169		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$
170	169	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$
171		df-ot	$⊢ ⟨g, h, i⟩ = ⟨⟨g, h⟩, i⟩$
172		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 ⟨g, h, i⟩ \in s) \land g \neq a) \to ⟨g, h, i⟩ \in s$
173	171 172	eqeltrrid	$⊢ ((((((φ \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, h⟩, i⟩ \in s$
174		opex	$⊢ ⟨g, h⟩ \in V$
175	174 99	opeldm	$⊢ ⟨⟨g, h⟩, i⟩ \in s \to ⟨g, h⟩ \in dom s$
176		vex	$⊢ g \in V$
177	176 136	opeldm	$⊢ ⟨g, h⟩ \in dom s \to g \in dom dom s$
178	173 175 177	3syl	$⊢ ((((((φ \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$
179	168 170 178	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$
180		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$
181	180	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$
182		ioran	$⊢ \neg (g R a \lor g = a) \leftrightarrow (\neg g R a \land \neg g = a)$
183	179 181 182	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)$
184	183	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))$
185	184	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))$
186	166 185	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))$
187	186	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)))$
188		eleq1	$⊢ q = ⟨g, h, i⟩ \to (q \in s \leftrightarrow ⟨g, h, i⟩ \in s)$
189	188	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))$
190		breq1	$⊢ q = ⟨g, h, i⟩ \to (q U ⟨a, b, c⟩ \leftrightarrow ⟨g, h, i⟩ U ⟨a, b, c⟩)$
191	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)))$
192	190 191	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))))$
193	192	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))))$
194	189 193	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)))))$
195	187 194	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⟩)$
196	195	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⟩)$
197	196	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⟩)$
198	197	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⟩)$
199	86 198	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⟩$
200	199	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⟩$
201		breq2	$⊢ p = ⟨a, b, c⟩ \to (q U p \leftrightarrow q U ⟨a, b, c⟩)$
202	201	notbid	$⊢ p = ⟨a, b, c⟩ \to (\neg q U p \leftrightarrow \neg q U ⟨a, b, c⟩)$
203	202	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⟩)$
204	203	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$
205	81 200 204	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$
206	74 205	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$
207	53 206	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$
208	36 207	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$
209	208	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)$
210	209	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)$
211		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)$
212	210 211	sylibr	$⊢ φ \to U Fr ((A \times B) \times C)$

Metamath Proof Explorer

Theorem frxp3

Proof