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	biimpri	$⊢ ⟨a, f⟩ \in s \to f \in s [\{a\}]$
74	73	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 ⟨a, f⟩ \in s) \to f \in s [\{a\}]$
75	69 70 74	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$
76	75	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)$
77		opeq1	$⊢ e = a \to ⟨e, f⟩ = ⟨a, f⟩$
78	77	eleq1d	$⊢ e = a \to (⟨e, f⟩ \in s \leftrightarrow ⟨a, f⟩ \in s)$
79	78	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))$
80		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)))$
81		olc	$⊢ e = a \to (e R a \lor e = a)$
82	81	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))))$
83		neeq1	$⊢ e = a \to (e \neq a \leftrightarrow a \neq a)$
84	83	orbi1d	$⊢ e = a \to ((e \neq a \lor f \neq c) \leftrightarrow (a \neq a \lor f \neq c))$
85		neirr	$⊢ \neg a \neq a$
86	85	biorfi	$⊢ f \neq c \leftrightarrow (a \neq a \lor f \neq c)$
87	84 86	bitr4di	$⊢ e = a \to ((e \neq a \lor f \neq c) \leftrightarrow f \neq c)$
88	87	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))$
89		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))$
90		nonconne	$⊢ \neg (f = c \land f \neq c)$
91	90	biorfri	$⊢ (f S c \land f \neq c) \leftrightarrow ((f S c \land f \neq c) \lor (f = c \land f \neq c))$
92	89 91	bitr4i	$⊢ ((f S c \lor f = c) \land f \neq c) \leftrightarrow (f S c \land f \neq c)$
93	88 92	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))$
94	82 93	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))$
95	80 94	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))$
96	95	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))$
97	79 96	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)))$
98	76 97	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)))$
99	98	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))$
100		breq1	$⊢ b = e \to (b R a \leftrightarrow e R a)$
101	100	notbid	$⊢ b = e \to (\neg b R a \leftrightarrow \neg e R a)$
102		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$
103	102	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$
104		vex	$⊢ e \in V$
105	104 71	opeldm	$⊢ ⟨e, f⟩ \in s \to e \in dom s$
106	105	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$
107	106	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$
108	101 103 107	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$
109		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$
110	109	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$
111		ioran	$⊢ \neg (e R a \lor e = a) \leftrightarrow (\neg e R a \land \neg e = a)$
112	108 110 111	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)$
113	112	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))$
114	99 113	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))$
115	114	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)))$
116		eleq1	$⊢ q = ⟨e, f⟩ \to (q \in s \leftrightarrow ⟨e, f⟩ \in s)$
117	116	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))$
118		breq1	$⊢ q = ⟨e, f⟩ \to (q T ⟨a, c⟩ \leftrightarrow ⟨e, f⟩ T ⟨a, c⟩)$
119	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)))$
120	118 119	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))))$
121	120	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))))$
122	117 121	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)))))$
123	115 122	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⟩)$
124	123	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⟩)$
125	124	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⟩)$
126	67 125	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⟩$
127	126	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⟩$
128	59 64 127	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$
129	56 128	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$
130	30 129	rexlimddv	$⊢ (φ \land (s \subseteq A \times B \land s \neq \emptyset)) \to \exists p \in s \forall q \in s \neg q T p$
131	130	ex	$⊢ φ \to ((s \subseteq A \times B \land s \neq \emptyset) \to \exists p \in s \forall q \in s \neg q T p)$
132	131	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)$
133		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)$
134	132 133	sylibr	$⊢ φ \to T Fr (A \times B)$

Metamath Proof Explorer

Theorem frxp2

Proof