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

Metamath Proof Explorer

Theorem frxp2

Proof