frxp2

Description: Another way of giving a well-founded order to a Cartesian product of two classes. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypotheses	xpord2.1	$⊢ T = \{⟨x, y⟩ \| (x \in (A \times B) \land y \in (A \times B) \land ((1^{st} (x) R 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) S 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}$
	frxp2.1	$⊢ φ \to R Fr A$
	frxp2.2	$⊢ φ \to S Fr B$
Assertion	frxp2	$⊢ φ \to T Fr (A \times B)$

Proof

Step	Hyp	Ref	Expression
1		xpord2.1	$⊢ T = \{⟨x, y⟩ \| (x \in (A \times B) \land y \in (A \times B) \land ((1^{st} (x) R 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) S 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}$
2		frxp2.1	$⊢ φ \to R Fr A$
3		frxp2.2	$⊢ φ \to S Fr B$
4		dmss	$⊢ s \subseteq A \times B \to dom s \subseteq dom (A \times B)$
5	4	ad2antrl	$⊢ (φ \land (s \subseteq A \times B \land s \neq \emptyset)) \to dom s \subseteq dom (A \times B)$
6		dmxpss	$⊢ dom (A \times B) \subseteq A$
7	5 6	sstrdi	$⊢ (φ \land (s \subseteq A \times B \land s \neq \emptyset)) \to dom s \subseteq A$
8		simprr	$⊢ (φ \land (s \subseteq A \times B \land s \neq \emptyset)) \to s \neq \emptyset$
9		relxp	$⊢ Rel (A \times B)$
10		relss	$⊢ s \subseteq A \times B \to (Rel (A \times B) \to Rel s)$
11	9 10	mpi	$⊢ s \subseteq A \times B \to Rel s$
12	11	ad2antrl	$⊢ (φ \land (s \subseteq A \times B \land s \neq \emptyset)) \to Rel s$
13		reldm0	$⊢ Rel s \to (s = \emptyset \leftrightarrow dom s = \emptyset)$
14	12 13	syl	$⊢ (φ \land (s \subseteq A \times B \land s \neq \emptyset)) \to (s = \emptyset \leftrightarrow dom s = \emptyset)$
15	14	necon3bid	$⊢ (φ \land (s \subseteq A \times B \land s \neq \emptyset)) \to (s \neq \emptyset \leftrightarrow dom s \neq \emptyset)$
16	8 15	mpbid	$⊢ (φ \land (s \subseteq A \times B \land s \neq \emptyset)) \to dom s \neq \emptyset$
17	2	adantr	$⊢ (φ \land (s \subseteq A \times B \land s \neq \emptyset)) \to R Fr A$
18		df-fr	$⊢ R Fr A \leftrightarrow \forall c ((c \subseteq A \land c \neq \emptyset) \to \exists a \in c \forall b \in c \neg b R a)$
19	17 18	sylib	$⊢ (φ \land (s \subseteq A \times B \land s \neq \emptyset)) \to \forall c ((c \subseteq A \land c \neq \emptyset) \to \exists a \in c \forall b \in c \neg b R a)$
20		vex	$⊢ s \in V$
21	20	dmex	$⊢ dom s \in V$
22		sseq1	$⊢ c = dom s \to (c \subseteq A \leftrightarrow dom s \subseteq A)$
23		neeq1	$⊢ c = dom s \to (c \neq \emptyset \leftrightarrow dom s \neq \emptyset)$
24	22 23	anbi12d	$⊢ c = dom s \to ((c \subseteq A \land c \neq \emptyset) \leftrightarrow (dom s \subseteq A \land dom s \neq \emptyset))$
25		raleq	$⊢ c = dom s \to (\forall b \in c \neg b R a \leftrightarrow \forall b \in dom s \neg b R a)$
26	25	rexeqbi1dv	$⊢ c = dom s \to (\exists a \in c \forall b \in c \neg b R a \leftrightarrow \exists a \in dom s \forall b \in dom s \neg b R a)$
27	24 26	imbi12d	$⊢ c = dom s \to (((c \subseteq A \land c \neq \emptyset) \to \exists a \in c \forall b \in c \neg b R a) \leftrightarrow ((dom s \subseteq A \land dom s \neq \emptyset) \to \exists a \in dom s \forall b \in dom s \neg b R a))$
28	21 27	spcv	$⊢ \forall c ((c \subseteq A \land c \neq \emptyset) \to \exists a \in c \forall b \in c \neg b R a) \to ((dom s \subseteq A \land dom s \neq \emptyset) \to \exists a \in dom s \forall b \in dom s \neg b R a)$
29	19 28	syl	$⊢ (φ \land (s \subseteq A \times B \land s \neq \emptyset)) \to ((dom s \subseteq A \land dom s \neq \emptyset) \to \exists a \in dom s \forall b \in dom s \neg b R a)$
30	7 16 29	mp2and	$⊢ (φ \land (s \subseteq A \times B \land s \neq \emptyset)) \to \exists a \in dom s \forall b \in dom s \neg b R a$
31		imassrn	$⊢ s [\{a\}] \subseteq ran s$
32		rnss	$⊢ s \subseteq A \times B \to ran s \subseteq ran (A \times B)$
33	32	ad2antrl	$⊢ (φ \land (s \subseteq A \times B \land s \neq \emptyset)) \to ran s \subseteq ran (A \times B)$
34	33	adantr	$⊢ ((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \to ran s \subseteq ran (A \times B)$
35		rnxpss	$⊢ ran (A \times B) \subseteq B$
36	34 35	sstrdi	$⊢ ((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \to ran s \subseteq B$
37	31 36	sstrid	$⊢ ((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \to s [\{a\}] \subseteq B$
38		simprl	$⊢ ((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \to a \in dom s$
39		imadisj	$⊢ s [\{a\}] = \emptyset \leftrightarrow dom s \cap \{a\} = \emptyset$
40		disjsn	$⊢ dom s \cap \{a\} = \emptyset \leftrightarrow \neg a \in dom s$
41	39 40	bitri	$⊢ s [\{a\}] = \emptyset \leftrightarrow \neg a \in dom s$
42	41	necon2abii	$⊢ a \in dom s \leftrightarrow s [\{a\}] \neq \emptyset$
43	38 42	sylib	$⊢ ((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \to s [\{a\}] \neq \emptyset$
44		df-fr	$⊢ S Fr B \leftrightarrow \forall e ((e \subseteq B \land e \neq \emptyset) \to \exists c \in e \forall d \in e \neg d S c)$
45	3 44	sylib	$⊢ φ \to \forall e ((e \subseteq B \land e \neq \emptyset) \to \exists c \in e \forall d \in e \neg d S c)$
46	45	ad2antrr	$⊢ ((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \to \forall e ((e \subseteq B \land e \neq \emptyset) \to \exists c \in e \forall d \in e \neg d S c)$
47	20	imaex	$⊢ s [\{a\}] \in V$
48		sseq1	$⊢ e = s [\{a\}] \to (e \subseteq B \leftrightarrow s [\{a\}] \subseteq B)$
49		neeq1	$⊢ e = s [\{a\}] \to (e \neq \emptyset \leftrightarrow s [\{a\}] \neq \emptyset)$
50	48 49	anbi12d	$⊢ e = s [\{a\}] \to ((e \subseteq B \land e \neq \emptyset) \leftrightarrow (s [\{a\}] \subseteq B \land s [\{a\}] \neq \emptyset))$
51		raleq	$⊢ e = s [\{a\}] \to (\forall d \in e \neg d S c \leftrightarrow \forall d \in s [\{a\}] \neg d S c)$
52	51	rexeqbi1dv	$⊢ e = s [\{a\}] \to (\exists c \in e \forall d \in e \neg d S c \leftrightarrow \exists c \in s [\{a\}] \forall d \in s [\{a\}] \neg d S c)$
53	50 52	imbi12d	$⊢ e = s [\{a\}] \to (((e \subseteq B \land e \neq \emptyset) \to \exists c \in e \forall d \in e \neg d S c) \leftrightarrow ((s [\{a\}] \subseteq B \land s [\{a\}] \neq \emptyset) \to \exists c \in s [\{a\}] \forall d \in s [\{a\}] \neg d S c))$
54	47 53	spcv	$⊢ \forall e ((e \subseteq B \land e \neq \emptyset) \to \exists c \in e \forall d \in e \neg d S c) \to ((s [\{a\}] \subseteq B \land s [\{a\}] \neq \emptyset) \to \exists c \in s [\{a\}] \forall d \in s [\{a\}] \neg d S c)$
55	46 54	syl	$⊢ ((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \to ((s [\{a\}] \subseteq B \land s [\{a\}] \neq \emptyset) \to \exists c \in s [\{a\}] \forall d \in s [\{a\}] \neg d S c)$
56	37 43 55	mp2and	$⊢ ((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \to \exists c \in s [\{a\}] \forall d \in s [\{a\}] \neg d S c$
57		breq2	$⊢ p = ⟨a, c⟩ \to (q T p \leftrightarrow q T ⟨a, c⟩)$
58	57	notbid	$⊢ p = ⟨a, c⟩ \to (\neg q T p \leftrightarrow \neg q T ⟨a, c⟩)$
59	58	ralbidv	$⊢ p = ⟨a, c⟩ \to (\forall q \in s \neg q T p \leftrightarrow \forall q \in s \neg q T ⟨a, c⟩)$
60		simprl	$⊢ (((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \to c \in s [\{a\}]$
61		vex	$⊢ a \in V$
62		vex	$⊢ c \in V$
63	61 62	elimasn	$⊢ c \in s [\{a\}] \leftrightarrow ⟨a, c⟩ \in s$
64	60 63	sylib	$⊢ (((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \to ⟨a, c⟩ \in s$
65	12	ad2antrr	$⊢ (((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \to Rel s$
66		elrel	$⊢ (Rel s \land q \in s) \to \exists e \exists f q = ⟨e, f⟩$
67	65 66	sylan	$⊢ ((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land q \in s) \to \exists e \exists f q = ⟨e, f⟩$
68		breq1	$⊢ d = f \to (d S c \leftrightarrow f S c)$
69	68	notbid	$⊢ d = f \to (\neg d S c \leftrightarrow \neg f S c)$
70		simplrr	$⊢ ((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨a, f⟩ \in s) \to \forall d \in s [\{a\}] \neg d S c$
71		vex	$⊢ f \in V$
72	61 71	elimasn	$⊢ f \in s [\{a\}] \leftrightarrow ⟨a, f⟩ \in s$
73	72	bilanri	$⊢ ((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨a, f⟩ \in s) \to f \in s [\{a\}]$
74	69 70 73	rspcdva	$⊢ ((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨a, f⟩ \in s) \to \neg f S c$
75	74	intnanrd	$⊢ ((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨a, f⟩ \in s) \to \neg (f S c \land f \neq c)$
76		opeq1	$⊢ e = a \to ⟨e, f⟩ = ⟨a, f⟩$
77	76	eleq1d	$⊢ e = a \to (⟨e, f⟩ \in s \leftrightarrow ⟨a, f⟩ \in s)$
78	77	anbi2d	$⊢ e = a \to (((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s) \leftrightarrow ((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨a, f⟩ \in s))$
79		3anass	$⊢ ((e R a \lor e = a) \land (f S c \lor f = c) \land (e \neq a \lor f \neq c)) \leftrightarrow ((e R a \lor e = a) \land ((f S c \lor f = c) \land (e \neq a \lor f \neq c)))$
80		olc	$⊢ e = a \to (e R a \lor e = a)$
81	80	biantrurd	$⊢ e = a \to (((f S c \lor f = c) \land (e \neq a \lor f \neq c)) \leftrightarrow ((e R a \lor e = a) \land ((f S c \lor f = c) \land (e \neq a \lor f \neq c))))$
82		neeq1	$⊢ e = a \to (e \neq a \leftrightarrow a \neq a)$
83	82	orbi1d	$⊢ e = a \to ((e \neq a \lor f \neq c) \leftrightarrow (a \neq a \lor f \neq c))$
84		neirr	$⊢ \neg a \neq a$
85	84	biorfi	$⊢ f \neq c \leftrightarrow (a \neq a \lor f \neq c)$
86	83 85	bitr4di	$⊢ e = a \to ((e \neq a \lor f \neq c) \leftrightarrow f \neq c)$
87	86	anbi2d	$⊢ e = a \to (((f S c \lor f = c) \land (e \neq a \lor f \neq c)) \leftrightarrow ((f S c \lor f = c) \land f \neq c))$
88		andir	$⊢ ((f S c \lor f = c) \land f \neq c) \leftrightarrow ((f S c \land f \neq c) \lor (f = c \land f \neq c))$
89		nonconne	$⊢ \neg (f = c \land f \neq c)$
90	89	biorfri	$⊢ (f S c \land f \neq c) \leftrightarrow ((f S c \land f \neq c) \lor (f = c \land f \neq c))$
91	88 90	bitr4i	$⊢ ((f S c \lor f = c) \land f \neq c) \leftrightarrow (f S c \land f \neq c)$
92	87 91	bitrdi	$⊢ e = a \to (((f S c \lor f = c) \land (e \neq a \lor f \neq c)) \leftrightarrow (f S c \land f \neq c))$
93	81 92	bitr3d	$⊢ e = a \to (((e R a \lor e = a) \land ((f S c \lor f = c) \land (e \neq a \lor f \neq c))) \leftrightarrow (f S c \land f \neq c))$
94	79 93	bitrid	$⊢ e = a \to (((e R a \lor e = a) \land (f S c \lor f = c) \land (e \neq a \lor f \neq c)) \leftrightarrow (f S c \land f \neq c))$
95	94	notbid	$⊢ e = a \to (\neg ((e R a \lor e = a) \land (f S c \lor f = c) \land (e \neq a \lor f \neq c)) \leftrightarrow \neg (f S c \land f \neq c))$
96	78 95	imbi12d	$⊢ e = a \to ((((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s) \to \neg ((e R a \lor e = a) \land (f S c \lor f = c) \land (e \neq a \lor f \neq c))) \leftrightarrow (((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨a, f⟩ \in s) \to \neg (f S c \land f \neq c)))$
97	75 96	mpbiri	$⊢ e = a \to (((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s) \to \neg ((e R a \lor e = a) \land (f S c \lor f = c) \land (e \neq a \lor f \neq c)))$
98	97	impcom	$⊢ (((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s) \land e = a) \to \neg ((e R a \lor e = a) \land (f S c \lor f = c) \land (e \neq a \lor f \neq c))$
99		breq1	$⊢ b = e \to (b R a \leftrightarrow e R a)$
100	99	notbid	$⊢ b = e \to (\neg b R a \leftrightarrow \neg e R a)$
101		simplrr	$⊢ (((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \to \forall b \in dom s \neg b R a$
102	101	ad2antrr	$⊢ (((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s) \land e \neq a) \to \forall b \in dom s \neg b R a$
103		vex	$⊢ e \in V$
104	103 71	opeldm	$⊢ ⟨e, f⟩ \in s \to e \in dom s$
105	104	adantl	$⊢ ((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s) \to e \in dom s$
106	105	adantr	$⊢ (((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s) \land e \neq a) \to e \in dom s$
107	100 102 106	rspcdva	$⊢ (((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s) \land e \neq a) \to \neg e R a$
108		simpr	$⊢ (((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s) \land e \neq a) \to e \neq a$
109	108	neneqd	$⊢ (((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s) \land e \neq a) \to \neg e = a$
110		ioran	$⊢ \neg (e R a \lor e = a) \leftrightarrow (\neg e R a \land \neg e = a)$
111	107 109 110	sylanbrc	$⊢ (((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s) \land e \neq a) \to \neg (e R a \lor e = a)$
112	111	intn3an1d	$⊢ (((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s) \land e \neq a) \to \neg ((e R a \lor e = a) \land (f S c \lor f = c) \land (e \neq a \lor f \neq c))$
113	98 112	pm2.61dane	$⊢ ((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s) \to \neg ((e R a \lor e = a) \land (f S c \lor f = c) \land (e \neq a \lor f \neq c))$
114	113	intn3an3d	$⊢ ((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s) \to \neg ((e \in A \land f \in B) \land (a \in A \land c \in B) \land ((e R a \lor e = a) \land (f S c \lor f = c) \land (e \neq a \lor f \neq c)))$
115		eleq1	$⊢ q = ⟨e, f⟩ \to (q \in s \leftrightarrow ⟨e, f⟩ \in s)$
116	115	anbi2d	$⊢ q = ⟨e, f⟩ \to (((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land q \in s) \leftrightarrow ((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s))$
117		breq1	$⊢ q = ⟨e, f⟩ \to (q T ⟨a, c⟩ \leftrightarrow ⟨e, f⟩ T ⟨a, c⟩)$
118	1	xpord2lem	$⊢ ⟨e, f⟩ T ⟨a, c⟩ \leftrightarrow ((e \in A \land f \in B) \land (a \in A \land c \in B) \land ((e R a \lor e = a) \land (f S c \lor f = c) \land (e \neq a \lor f \neq c)))$
119	117 118	bitrdi	$⊢ q = ⟨e, f⟩ \to (q T ⟨a, c⟩ \leftrightarrow ((e \in A \land f \in B) \land (a \in A \land c \in B) \land ((e R a \lor e = a) \land (f S c \lor f = c) \land (e \neq a \lor f \neq c))))$
120	119	notbid	$⊢ q = ⟨e, f⟩ \to (\neg q T ⟨a, c⟩ \leftrightarrow \neg ((e \in A \land f \in B) \land (a \in A \land c \in B) \land ((e R a \lor e = a) \land (f S c \lor f = c) \land (e \neq a \lor f \neq c))))$
121	116 120	imbi12d	$⊢ q = ⟨e, f⟩ \to ((((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land q \in s) \to \neg q T ⟨a, c⟩) \leftrightarrow (((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land ⟨e, f⟩ \in s) \to \neg ((e \in A \land f \in B) \land (a \in A \land c \in B) \land ((e R a \lor e = a) \land (f S c \lor f = c) \land (e \neq a \lor f \neq c)))))$
122	114 121	mpbiri	$⊢ q = ⟨e, f⟩ \to (((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land q \in s) \to \neg q T ⟨a, c⟩)$
123	122	com12	$⊢ ((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land q \in s) \to (q = ⟨e, f⟩ \to \neg q T ⟨a, c⟩)$
124	123	exlimdvv	$⊢ ((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land q \in s) \to (\exists e \exists f q = ⟨e, f⟩ \to \neg q T ⟨a, c⟩)$
125	67 124	mpd	$⊢ ((((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \land q \in s) \to \neg q T ⟨a, c⟩$
126	125	ralrimiva	$⊢ (((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \to \forall q \in s \neg q T ⟨a, c⟩$
127	59 64 126	rspcedvdw	$⊢ (((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \land (c \in s [\{a\}] \land \forall d \in s [\{a\}] \neg d S c)) \to \exists p \in s \forall q \in s \neg q T p$
128	56 127	rexlimddv	$⊢ ((φ \land (s \subseteq A \times B \land s \neq \emptyset)) \land (a \in dom s \land \forall b \in dom s \neg b R a)) \to \exists p \in s \forall q \in s \neg q T p$
129	30 128	rexlimddv	$⊢ (φ \land (s \subseteq A \times B \land s \neq \emptyset)) \to \exists p \in s \forall q \in s \neg q T p$
130	129	ex	$⊢ φ \to ((s \subseteq A \times B \land s \neq \emptyset) \to \exists p \in s \forall q \in s \neg q T p)$
131	130	alrimiv	$⊢ φ \to \forall s ((s \subseteq A \times B \land s \neq \emptyset) \to \exists p \in s \forall q \in s \neg q T p)$
132		df-fr	$⊢ T Fr (A \times B) \leftrightarrow \forall s ((s \subseteq A \times B \land s \neq \emptyset) \to \exists p \in s \forall q \in s \neg q T p)$
133	131 132	sylibr	$⊢ φ \to T Fr (A \times B)$

Metamath Proof Explorer

Theorem frxp2

Proof