frxp

Description: A lexicographical ordering of two well-founded classes. (Contributed by Scott Fenton, 17-Mar-2011) (Revised by Mario Carneiro, 7-Mar-2013) (Proof shortened by Wolf Lammen, 4-Oct-2014)

		Ref	Expression
	Hypothesis	frxp.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))))\}$
	Assertion	frxp	$⊢ (R Fr A \land S Fr B) \to T Fr (A \times B)$

Proof

Step	Hyp	Ref	Expression
1		frxp.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))))\}$
2		ssn0	$⊢ (s \subseteq A \times B \land s \neq \emptyset) \to A \times B \neq \emptyset$
3		xpnz	$⊢ (A \neq \emptyset \land B \neq \emptyset) \leftrightarrow A \times B \neq \emptyset$
4	3	biimpri	$⊢ A \times B \neq \emptyset \to (A \neq \emptyset \land B \neq \emptyset)$
5	4	simprd	$⊢ A \times B \neq \emptyset \to B \neq \emptyset$
6	2 5	syl	$⊢ (s \subseteq A \times B \land s \neq \emptyset) \to B \neq \emptyset$
7		dmxp	$⊢ B \neq \emptyset \to dom (A \times B) = A$
8		dmss	$⊢ s \subseteq A \times B \to dom s \subseteq dom (A \times B)$
9		sseq2	$⊢ dom (A \times B) = A \to (dom s \subseteq dom (A \times B) \leftrightarrow dom s \subseteq A)$
10	8 9	syl5ib	$⊢ dom (A \times B) = A \to (s \subseteq A \times B \to dom s \subseteq A)$
11	7 10	syl	$⊢ B \neq \emptyset \to (s \subseteq A \times B \to dom s \subseteq A)$
12	11	impcom	$⊢ (s \subseteq A \times B \land B \neq \emptyset) \to dom s \subseteq A$
13	6 12	syldan	$⊢ (s \subseteq A \times B \land s \neq \emptyset) \to dom s \subseteq A$
14		relxp	$⊢ Rel (A \times B)$
15		relss	$⊢ s \subseteq A \times B \to (Rel (A \times B) \to Rel s)$
16	14 15	mpi	$⊢ s \subseteq A \times B \to Rel s$
17		reldm0	$⊢ Rel s \to (s = \emptyset \leftrightarrow dom s = \emptyset)$
18	16 17	syl	$⊢ s \subseteq A \times B \to (s = \emptyset \leftrightarrow dom s = \emptyset)$
19	18	necon3bid	$⊢ s \subseteq A \times B \to (s \neq \emptyset \leftrightarrow dom s \neq \emptyset)$
20	19	biimpa	$⊢ (s \subseteq A \times B \land s \neq \emptyset) \to dom s \neq \emptyset$
21	13 20	jca	$⊢ (s \subseteq A \times B \land s \neq \emptyset) \to (dom s \subseteq A \land dom s \neq \emptyset)$
22		df-fr	$⊢ R Fr A \leftrightarrow \forall v ((v \subseteq A \land v \neq \emptyset) \to \exists a \in v \forall c \in v \neg c R a)$
23		vex	$⊢ s \in V$
24	23	dmex	$⊢ dom s \in V$
25		sseq1	$⊢ v = dom s \to (v \subseteq A \leftrightarrow dom s \subseteq A)$
26		neeq1	$⊢ v = dom s \to (v \neq \emptyset \leftrightarrow dom s \neq \emptyset)$
27	25 26	anbi12d	$⊢ v = dom s \to ((v \subseteq A \land v \neq \emptyset) \leftrightarrow (dom s \subseteq A \land dom s \neq \emptyset))$
28		raleq	$⊢ v = dom s \to (\forall c \in v \neg c R a \leftrightarrow \forall c \in dom s \neg c R a)$
29	28	rexeqbi1dv	$⊢ v = dom s \to (\exists a \in v \forall c \in v \neg c R a \leftrightarrow \exists a \in dom s \forall c \in dom s \neg c R a)$
30	27 29	imbi12d	$⊢ v = dom s \to (((v \subseteq A \land v \neq \emptyset) \to \exists a \in v \forall c \in v \neg c R a) \leftrightarrow ((dom s \subseteq A \land dom s \neq \emptyset) \to \exists a \in dom s \forall c \in dom s \neg c R a))$
31	24 30	spcv	$⊢ \forall v ((v \subseteq A \land v \neq \emptyset) \to \exists a \in v \forall c \in v \neg c R a) \to ((dom s \subseteq A \land dom s \neq \emptyset) \to \exists a \in dom s \forall c \in dom s \neg c R a)$
32	22 31	sylbi	$⊢ R Fr A \to ((dom s \subseteq A \land dom s \neq \emptyset) \to \exists a \in dom s \forall c \in dom s \neg c R a)$
33	21 32	syl5	$⊢ R Fr A \to ((s \subseteq A \times B \land s \neq \emptyset) \to \exists a \in dom s \forall c \in dom s \neg c R a)$
34	33	adantr	$⊢ (R Fr A \land S Fr B) \to ((s \subseteq A \times B \land s \neq \emptyset) \to \exists a \in dom s \forall c \in dom s \neg c R a)$
35		imassrn	$⊢ s [\{a\}] \subseteq ran s$
36		xpeq0	$⊢ A \times B = \emptyset \leftrightarrow (A = \emptyset \lor B = \emptyset)$
37	36	biimpri	$⊢ (A = \emptyset \lor B = \emptyset) \to A \times B = \emptyset$
38	37	orcs	$⊢ A = \emptyset \to A \times B = \emptyset$
39		sseq2	$⊢ A \times B = \emptyset \to (s \subseteq A \times B \leftrightarrow s \subseteq \emptyset)$
40		ss0	$⊢ s \subseteq \emptyset \to s = \emptyset$
41	39 40	syl6bi	$⊢ A \times B = \emptyset \to (s \subseteq A \times B \to s = \emptyset)$
42	38 41	syl	$⊢ A = \emptyset \to (s \subseteq A \times B \to s = \emptyset)$
43		rneq	$⊢ s = \emptyset \to ran s = ran \emptyset$
44		rn0	$⊢ ran \emptyset = \emptyset$
45		0ss	$⊢ \emptyset \subseteq B$
46	44 45	eqsstri	$⊢ ran \emptyset \subseteq B$
47	43 46	eqsstrdi	$⊢ s = \emptyset \to ran s \subseteq B$
48	42 47	syl6	$⊢ A = \emptyset \to (s \subseteq A \times B \to ran s \subseteq B)$
49		rnxp	$⊢ A \neq \emptyset \to ran (A \times B) = B$
50		rnss	$⊢ s \subseteq A \times B \to ran s \subseteq ran (A \times B)$
51		sseq2	$⊢ ran (A \times B) = B \to (ran s \subseteq ran (A \times B) \leftrightarrow ran s \subseteq B)$
52	50 51	syl5ib	$⊢ ran (A \times B) = B \to (s \subseteq A \times B \to ran s \subseteq B)$
53	49 52	syl	$⊢ A \neq \emptyset \to (s \subseteq A \times B \to ran s \subseteq B)$
54	48 53	pm2.61ine	$⊢ s \subseteq A \times B \to ran s \subseteq B$
55	35 54	sstrid	$⊢ s \subseteq A \times B \to s [\{a\}] \subseteq B$
56		vex	$⊢ a \in V$
57	56	eldm	$⊢ a \in dom s \leftrightarrow \exists b a s b$
58		vex	$⊢ b \in V$
59	56 58	elimasn	$⊢ b \in s [\{a\}] \leftrightarrow ⟨a, b⟩ \in s$
60		df-br	$⊢ a s b \leftrightarrow ⟨a, b⟩ \in s$
61	59 60	bitr4i	$⊢ b \in s [\{a\}] \leftrightarrow a s b$
62		ne0i	$⊢ b \in s [\{a\}] \to s [\{a\}] \neq \emptyset$
63	61 62	sylbir	$⊢ a s b \to s [\{a\}] \neq \emptyset$
64	63	exlimiv	$⊢ \exists b a s b \to s [\{a\}] \neq \emptyset$
65	57 64	sylbi	$⊢ a \in dom s \to s [\{a\}] \neq \emptyset$
66		df-fr	$⊢ S Fr B \leftrightarrow \forall v ((v \subseteq B \land v \neq \emptyset) \to \exists b \in v \forall d \in v \neg d S b)$
67	23	imaex	$⊢ s [\{a\}] \in V$
68		sseq1	$⊢ v = s [\{a\}] \to (v \subseteq B \leftrightarrow s [\{a\}] \subseteq B)$
69		neeq1	$⊢ v = s [\{a\}] \to (v \neq \emptyset \leftrightarrow s [\{a\}] \neq \emptyset)$
70	68 69	anbi12d	$⊢ v = s [\{a\}] \to ((v \subseteq B \land v \neq \emptyset) \leftrightarrow (s [\{a\}] \subseteq B \land s [\{a\}] \neq \emptyset))$
71		raleq	$⊢ v = s [\{a\}] \to (\forall d \in v \neg d S b \leftrightarrow \forall d \in s [\{a\}] \neg d S b)$
72	71	rexeqbi1dv	$⊢ v = s [\{a\}] \to (\exists b \in v \forall d \in v \neg d S b \leftrightarrow \exists b \in s [\{a\}] \forall d \in s [\{a\}] \neg d S b)$
73	70 72	imbi12d	$⊢ v = s [\{a\}] \to (((v \subseteq B \land v \neq \emptyset) \to \exists b \in v \forall d \in v \neg d S b) \leftrightarrow ((s [\{a\}] \subseteq B \land s [\{a\}] \neq \emptyset) \to \exists b \in s [\{a\}] \forall d \in s [\{a\}] \neg d S b))$
74	67 73	spcv	$⊢ \forall v ((v \subseteq B \land v \neq \emptyset) \to \exists b \in v \forall d \in v \neg d S b) \to ((s [\{a\}] \subseteq B \land s [\{a\}] \neq \emptyset) \to \exists b \in s [\{a\}] \forall d \in s [\{a\}] \neg d S b)$
75	66 74	sylbi	$⊢ S Fr B \to ((s [\{a\}] \subseteq B \land s [\{a\}] \neq \emptyset) \to \exists b \in s [\{a\}] \forall d \in s [\{a\}] \neg d S b)$
76	55 65 75	syl2ani	$⊢ S Fr B \to ((s \subseteq A \times B \land a \in dom s) \to \exists b \in s [\{a\}] \forall d \in s [\{a\}] \neg d S b)$
77		1stdm	$⊢ (Rel s \land w \in s) \to 1^{st} (w) \in dom s$
78		breq1	$⊢ c = 1^{st} (w) \to (c R a \leftrightarrow 1^{st} (w) R a)$
79	78	notbid	$⊢ c = 1^{st} (w) \to (\neg c R a \leftrightarrow \neg 1^{st} (w) R a)$
80	79	rspccv	$⊢ \forall c \in dom s \neg c R a \to (1^{st} (w) \in dom s \to \neg 1^{st} (w) R a)$
81	77 80	syl5	$⊢ \forall c \in dom s \neg c R a \to ((Rel s \land w \in s) \to \neg 1^{st} (w) R a)$
82	81	expd	$⊢ \forall c \in dom s \neg c R a \to (Rel s \to (w \in s \to \neg 1^{st} (w) R a))$
83	82	impcom	$⊢ (Rel s \land \forall c \in dom s \neg c R a) \to (w \in s \to \neg 1^{st} (w) R a)$
84	83	adantr	$⊢ ((Rel s \land \forall c \in dom s \neg c R a) \land \forall d \in s [\{a\}] \neg d S b) \to (w \in s \to \neg 1^{st} (w) R a)$
85		elrel	$⊢ (Rel s \land w \in s) \to \exists t \exists u w = ⟨t, u⟩$
86	85	ex	$⊢ Rel s \to (w \in s \to \exists t \exists u w = ⟨t, u⟩)$
87	86	adantr	$⊢ (Rel s \land \forall d \in s [\{a\}] \neg d S b) \to (w \in s \to \exists t \exists u w = ⟨t, u⟩)$
88		vex	$⊢ u \in V$
89	56 88	elimasn	$⊢ u \in s [\{a\}] \leftrightarrow ⟨a, u⟩ \in s$
90		breq1	$⊢ d = u \to (d S b \leftrightarrow u S b)$
91	90	notbid	$⊢ d = u \to (\neg d S b \leftrightarrow \neg u S b)$
92	91	rspccv	$⊢ \forall d \in s [\{a\}] \neg d S b \to (u \in s [\{a\}] \to \neg u S b)$
93	89 92	syl5bir	$⊢ \forall d \in s [\{a\}] \neg d S b \to (⟨a, u⟩ \in s \to \neg u S b)$
94	93	adantl	$⊢ (Rel s \land \forall d \in s [\{a\}] \neg d S b) \to (⟨a, u⟩ \in s \to \neg u S b)$
95		opeq1	$⊢ t = a \to ⟨t, u⟩ = ⟨a, u⟩$
96	95	eleq1d	$⊢ t = a \to (⟨t, u⟩ \in s \leftrightarrow ⟨a, u⟩ \in s)$
97	96	imbi1d	$⊢ t = a \to ((⟨t, u⟩ \in s \to \neg u S b) \leftrightarrow (⟨a, u⟩ \in s \to \neg u S b))$
98	94 97	syl5ibr	$⊢ t = a \to ((Rel s \land \forall d \in s [\{a\}] \neg d S b) \to (⟨t, u⟩ \in s \to \neg u S b))$
99	98	com3l	$⊢ (Rel s \land \forall d \in s [\{a\}] \neg d S b) \to (⟨t, u⟩ \in s \to (t = a \to \neg u S b))$
100		eleq1	$⊢ w = ⟨t, u⟩ \to (w \in s \leftrightarrow ⟨t, u⟩ \in s)$
101		vex	$⊢ t \in V$
102	101 88	op1std	$⊢ w = ⟨t, u⟩ \to 1^{st} (w) = t$
103	102	eqeq1d	$⊢ w = ⟨t, u⟩ \to (1^{st} (w) = a \leftrightarrow t = a)$
104	101 88	op2ndd	$⊢ w = ⟨t, u⟩ \to 2^{nd} (w) = u$
105	104	breq1d	$⊢ w = ⟨t, u⟩ \to (2^{nd} (w) S b \leftrightarrow u S b)$
106	105	notbid	$⊢ w = ⟨t, u⟩ \to (\neg 2^{nd} (w) S b \leftrightarrow \neg u S b)$
107	103 106	imbi12d	$⊢ w = ⟨t, u⟩ \to ((1^{st} (w) = a \to \neg 2^{nd} (w) S b) \leftrightarrow (t = a \to \neg u S b))$
108	100 107	imbi12d	$⊢ w = ⟨t, u⟩ \to ((w \in s \to (1^{st} (w) = a \to \neg 2^{nd} (w) S b)) \leftrightarrow (⟨t, u⟩ \in s \to (t = a \to \neg u S b)))$
109	99 108	syl5ibr	$⊢ w = ⟨t, u⟩ \to ((Rel s \land \forall d \in s [\{a\}] \neg d S b) \to (w \in s \to (1^{st} (w) = a \to \neg 2^{nd} (w) S b)))$
110	109	exlimivv	$⊢ \exists t \exists u w = ⟨t, u⟩ \to ((Rel s \land \forall d \in s [\{a\}] \neg d S b) \to (w \in s \to (1^{st} (w) = a \to \neg 2^{nd} (w) S b)))$
111	110	com3l	$⊢ (Rel s \land \forall d \in s [\{a\}] \neg d S b) \to (w \in s \to (\exists t \exists u w = ⟨t, u⟩ \to (1^{st} (w) = a \to \neg 2^{nd} (w) S b)))$
112	87 111	mpdd	$⊢ (Rel s \land \forall d \in s [\{a\}] \neg d S b) \to (w \in s \to (1^{st} (w) = a \to \neg 2^{nd} (w) S b))$
113	112	adantlr	$⊢ ((Rel s \land \forall c \in dom s \neg c R a) \land \forall d \in s [\{a\}] \neg d S b) \to (w \in s \to (1^{st} (w) = a \to \neg 2^{nd} (w) S b))$
114	84 113	jcad	$⊢ ((Rel s \land \forall c \in dom s \neg c R a) \land \forall d \in s [\{a\}] \neg d S b) \to (w \in s \to (\neg 1^{st} (w) R a \land (1^{st} (w) = a \to \neg 2^{nd} (w) S b)))$
115	114	ralrimiv	$⊢ ((Rel s \land \forall c \in dom s \neg c R a) \land \forall d \in s [\{a\}] \neg d S b) \to \forall w \in s (\neg 1^{st} (w) R a \land (1^{st} (w) = a \to \neg 2^{nd} (w) S b))$
116	115	ex	$⊢ (Rel s \land \forall c \in dom s \neg c R a) \to (\forall d \in s [\{a\}] \neg d S b \to \forall w \in s (\neg 1^{st} (w) R a \land (1^{st} (w) = a \to \neg 2^{nd} (w) S b)))$
117	16 116	sylan	$⊢ (s \subseteq A \times B \land \forall c \in dom s \neg c R a) \to (\forall d \in s [\{a\}] \neg d S b \to \forall w \in s (\neg 1^{st} (w) R a \land (1^{st} (w) = a \to \neg 2^{nd} (w) S b)))$
118		olc	$⊢ (\neg 1^{st} (w) R a \land (1^{st} (w) = a \to \neg 2^{nd} (w) S b)) \to (\neg (w \in (A \times B) \land ⟨a, b⟩ \in (A \times B)) \lor (\neg 1^{st} (w) R a \land (1^{st} (w) = a \to \neg 2^{nd} (w) S b)))$
119	118	ralimi	$⊢ \forall w \in s (\neg 1^{st} (w) R a \land (1^{st} (w) = a \to \neg 2^{nd} (w) S b)) \to \forall w \in s (\neg (w \in (A \times B) \land ⟨a, b⟩ \in (A \times B)) \lor (\neg 1^{st} (w) R a \land (1^{st} (w) = a \to \neg 2^{nd} (w) S b)))$
120	117 119	syl6	$⊢ (s \subseteq A \times B \land \forall c \in dom s \neg c R a) \to (\forall d \in s [\{a\}] \neg d S b \to \forall w \in s (\neg (w \in (A \times B) \land ⟨a, b⟩ \in (A \times B)) \lor (\neg 1^{st} (w) R a \land (1^{st} (w) = a \to \neg 2^{nd} (w) S b))))$
121		ianor	$⊢ \neg ((w \in (A \times B) \land ⟨a, b⟩ \in (A \times B)) \land (1^{st} (w) R a \lor (1^{st} (w) = a \land 2^{nd} (w) S b))) \leftrightarrow (\neg (w \in (A \times B) \land ⟨a, b⟩ \in (A \times B)) \lor \neg (1^{st} (w) R a \lor (1^{st} (w) = a \land 2^{nd} (w) S b)))$
122		vex	$⊢ w \in V$
123		opex	$⊢ ⟨a, b⟩ \in V$
124		eleq1	$⊢ x = w \to (x \in (A \times B) \leftrightarrow w \in (A \times B))$
125	124	anbi1d	$⊢ x = w \to ((x \in (A \times B) \land y \in (A \times B)) \leftrightarrow (w \in (A \times B) \land y \in (A \times B)))$
126		fveq2	$⊢ x = w \to 1^{st} (x) = 1^{st} (w)$
127	126	breq1d	$⊢ x = w \to (1^{st} (x) R 1^{st} (y) \leftrightarrow 1^{st} (w) R 1^{st} (y))$
128	126	eqeq1d	$⊢ x = w \to (1^{st} (x) = 1^{st} (y) \leftrightarrow 1^{st} (w) = 1^{st} (y))$
129		fveq2	$⊢ x = w \to 2^{nd} (x) = 2^{nd} (w)$
130	129	breq1d	$⊢ x = w \to (2^{nd} (x) S 2^{nd} (y) \leftrightarrow 2^{nd} (w) S 2^{nd} (y))$
131	128 130	anbi12d	$⊢ x = w \to ((1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) S 2^{nd} (y)) \leftrightarrow (1^{st} (w) = 1^{st} (y) \land 2^{nd} (w) S 2^{nd} (y)))$
132	127 131	orbi12d	$⊢ x = w \to ((1^{st} (x) R 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) S 2^{nd} (y))) \leftrightarrow (1^{st} (w) R 1^{st} (y) \lor (1^{st} (w) = 1^{st} (y) \land 2^{nd} (w) S 2^{nd} (y))))$
133	125 132	anbi12d	$⊢ x = w \to (((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)))) \leftrightarrow ((w \in (A \times B) \land y \in (A \times B)) \land (1^{st} (w) R 1^{st} (y) \lor (1^{st} (w) = 1^{st} (y) \land 2^{nd} (w) S 2^{nd} (y)))))$
134		eleq1	$⊢ y = ⟨a, b⟩ \to (y \in (A \times B) \leftrightarrow ⟨a, b⟩ \in (A \times B))$
135	134	anbi2d	$⊢ y = ⟨a, b⟩ \to ((w \in (A \times B) \land y \in (A \times B)) \leftrightarrow (w \in (A \times B) \land ⟨a, b⟩ \in (A \times B)))$
136	56 58	op1std	$⊢ y = ⟨a, b⟩ \to 1^{st} (y) = a$
137	136	breq2d	$⊢ y = ⟨a, b⟩ \to (1^{st} (w) R 1^{st} (y) \leftrightarrow 1^{st} (w) R a)$
138	136	eqeq2d	$⊢ y = ⟨a, b⟩ \to (1^{st} (w) = 1^{st} (y) \leftrightarrow 1^{st} (w) = a)$
139	56 58	op2ndd	$⊢ y = ⟨a, b⟩ \to 2^{nd} (y) = b$
140	139	breq2d	$⊢ y = ⟨a, b⟩ \to (2^{nd} (w) S 2^{nd} (y) \leftrightarrow 2^{nd} (w) S b)$
141	138 140	anbi12d	$⊢ y = ⟨a, b⟩ \to ((1^{st} (w) = 1^{st} (y) \land 2^{nd} (w) S 2^{nd} (y)) \leftrightarrow (1^{st} (w) = a \land 2^{nd} (w) S b))$
142	137 141	orbi12d	$⊢ y = ⟨a, b⟩ \to ((1^{st} (w) R 1^{st} (y) \lor (1^{st} (w) = 1^{st} (y) \land 2^{nd} (w) S 2^{nd} (y))) \leftrightarrow (1^{st} (w) R a \lor (1^{st} (w) = a \land 2^{nd} (w) S b)))$
143	135 142	anbi12d	$⊢ y = ⟨a, b⟩ \to (((w \in (A \times B) \land y \in (A \times B)) \land (1^{st} (w) R 1^{st} (y) \lor (1^{st} (w) = 1^{st} (y) \land 2^{nd} (w) S 2^{nd} (y)))) \leftrightarrow ((w \in (A \times B) \land ⟨a, b⟩ \in (A \times B)) \land (1^{st} (w) R a \lor (1^{st} (w) = a \land 2^{nd} (w) S b))))$
144	122 123 133 143 1	brab	$⊢ w T ⟨a, b⟩ \leftrightarrow ((w \in (A \times B) \land ⟨a, b⟩ \in (A \times B)) \land (1^{st} (w) R a \lor (1^{st} (w) = a \land 2^{nd} (w) S b)))$
145	121 144	xchnxbir	$⊢ \neg w T ⟨a, b⟩ \leftrightarrow (\neg (w \in (A \times B) \land ⟨a, b⟩ \in (A \times B)) \lor \neg (1^{st} (w) R a \lor (1^{st} (w) = a \land 2^{nd} (w) S b)))$
146		ioran	$⊢ \neg (1^{st} (w) R a \lor (1^{st} (w) = a \land 2^{nd} (w) S b)) \leftrightarrow (\neg 1^{st} (w) R a \land \neg (1^{st} (w) = a \land 2^{nd} (w) S b))$
147		ianor	$⊢ \neg (1^{st} (w) = a \land 2^{nd} (w) S b) \leftrightarrow (\neg 1^{st} (w) = a \lor \neg 2^{nd} (w) S b)$
148		pm4.62	$⊢ (1^{st} (w) = a \to \neg 2^{nd} (w) S b) \leftrightarrow (\neg 1^{st} (w) = a \lor \neg 2^{nd} (w) S b)$
149	147 148	bitr4i	$⊢ \neg (1^{st} (w) = a \land 2^{nd} (w) S b) \leftrightarrow (1^{st} (w) = a \to \neg 2^{nd} (w) S b)$
150	149	anbi2i	$⊢ (\neg 1^{st} (w) R a \land \neg (1^{st} (w) = a \land 2^{nd} (w) S b)) \leftrightarrow (\neg 1^{st} (w) R a \land (1^{st} (w) = a \to \neg 2^{nd} (w) S b))$
151	146 150	bitri	$⊢ \neg (1^{st} (w) R a \lor (1^{st} (w) = a \land 2^{nd} (w) S b)) \leftrightarrow (\neg 1^{st} (w) R a \land (1^{st} (w) = a \to \neg 2^{nd} (w) S b))$
152	151	orbi2i	$⊢ (\neg (w \in (A \times B) \land ⟨a, b⟩ \in (A \times B)) \lor \neg (1^{st} (w) R a \lor (1^{st} (w) = a \land 2^{nd} (w) S b))) \leftrightarrow (\neg (w \in (A \times B) \land ⟨a, b⟩ \in (A \times B)) \lor (\neg 1^{st} (w) R a \land (1^{st} (w) = a \to \neg 2^{nd} (w) S b)))$
153	145 152	bitri	$⊢ \neg w T ⟨a, b⟩ \leftrightarrow (\neg (w \in (A \times B) \land ⟨a, b⟩ \in (A \times B)) \lor (\neg 1^{st} (w) R a \land (1^{st} (w) = a \to \neg 2^{nd} (w) S b)))$
154	153	ralbii	$⊢ \forall w \in s \neg w T ⟨a, b⟩ \leftrightarrow \forall w \in s (\neg (w \in (A \times B) \land ⟨a, b⟩ \in (A \times B)) \lor (\neg 1^{st} (w) R a \land (1^{st} (w) = a \to \neg 2^{nd} (w) S b)))$
155	120 154	syl6ibr	$⊢ (s \subseteq A \times B \land \forall c \in dom s \neg c R a) \to (\forall d \in s [\{a\}] \neg d S b \to \forall w \in s \neg w T ⟨a, b⟩)$
156	155	reximdv	$⊢ (s \subseteq A \times B \land \forall c \in dom s \neg c R a) \to (\exists b \in s [\{a\}] \forall d \in s [\{a\}] \neg d S b \to \exists b \in s [\{a\}] \forall w \in s \neg w T ⟨a, b⟩)$
157	156	ex	$⊢ s \subseteq A \times B \to (\forall c \in dom s \neg c R a \to (\exists b \in s [\{a\}] \forall d \in s [\{a\}] \neg d S b \to \exists b \in s [\{a\}] \forall w \in s \neg w T ⟨a, b⟩))$
158	157	com23	$⊢ s \subseteq A \times B \to (\exists b \in s [\{a\}] \forall d \in s [\{a\}] \neg d S b \to (\forall c \in dom s \neg c R a \to \exists b \in s [\{a\}] \forall w \in s \neg w T ⟨a, b⟩))$
159	158	adantr	$⊢ (s \subseteq A \times B \land a \in dom s) \to (\exists b \in s [\{a\}] \forall d \in s [\{a\}] \neg d S b \to (\forall c \in dom s \neg c R a \to \exists b \in s [\{a\}] \forall w \in s \neg w T ⟨a, b⟩))$
160	76 159	sylcom	$⊢ S Fr B \to ((s \subseteq A \times B \land a \in dom s) \to (\forall c \in dom s \neg c R a \to \exists b \in s [\{a\}] \forall w \in s \neg w T ⟨a, b⟩))$
161	160	impl	$⊢ ((S Fr B \land s \subseteq A \times B) \land a \in dom s) \to (\forall c \in dom s \neg c R a \to \exists b \in s [\{a\}] \forall w \in s \neg w T ⟨a, b⟩)$
162	161	expimpd	$⊢ (S Fr B \land s \subseteq A \times B) \to ((a \in dom s \land \forall c \in dom s \neg c R a) \to \exists b \in s [\{a\}] \forall w \in s \neg w T ⟨a, b⟩)$
163	162	3adant3	$⊢ (S Fr B \land s \subseteq A \times B \land s \neq \emptyset) \to ((a \in dom s \land \forall c \in dom s \neg c R a) \to \exists b \in s [\{a\}] \forall w \in s \neg w T ⟨a, b⟩)$
164		resss	$⊢ {s ↾}_{\{a\}} \subseteq s$
165		df-rex	$⊢ \exists b \in s [\{a\}] \forall w \in s \neg w T ⟨a, b⟩ \leftrightarrow \exists b (b \in s [\{a\}] \land \forall w \in s \neg w T ⟨a, b⟩)$
166		eqid	$⊢ ⟨a, b⟩ = ⟨a, b⟩$
167		eqeq1	$⊢ z = ⟨a, b⟩ \to (z = ⟨a, b⟩ \leftrightarrow ⟨a, b⟩ = ⟨a, b⟩)$
168		breq2	$⊢ z = ⟨a, b⟩ \to (w T z \leftrightarrow w T ⟨a, b⟩)$
169	168	notbid	$⊢ z = ⟨a, b⟩ \to (\neg w T z \leftrightarrow \neg w T ⟨a, b⟩)$
170	169	ralbidv	$⊢ z = ⟨a, b⟩ \to (\forall w \in s \neg w T z \leftrightarrow \forall w \in s \neg w T ⟨a, b⟩)$
171	170	anbi2d	$⊢ z = ⟨a, b⟩ \to ((⟨a, b⟩ \in s \land \forall w \in s \neg w T z) \leftrightarrow (⟨a, b⟩ \in s \land \forall w \in s \neg w T ⟨a, b⟩))$
172	167 171	anbi12d	$⊢ z = ⟨a, b⟩ \to ((z = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T z)) \leftrightarrow (⟨a, b⟩ = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T ⟨a, b⟩)))$
173	123 172	spcev	$⊢ (⟨a, b⟩ = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T ⟨a, b⟩)) \to \exists z (z = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T z))$
174	166 173	mpan	$⊢ (⟨a, b⟩ \in s \land \forall w \in s \neg w T ⟨a, b⟩) \to \exists z (z = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T z))$
175	59 174	sylanb	$⊢ (b \in s [\{a\}] \land \forall w \in s \neg w T ⟨a, b⟩) \to \exists z (z = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T z))$
176	175	eximi	$⊢ \exists b (b \in s [\{a\}] \land \forall w \in s \neg w T ⟨a, b⟩) \to \exists b \exists z (z = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T z))$
177	165 176	sylbi	$⊢ \exists b \in s [\{a\}] \forall w \in s \neg w T ⟨a, b⟩ \to \exists b \exists z (z = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T z))$
178		excom	$⊢ \exists b \exists z (z = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T z)) \leftrightarrow \exists z \exists b (z = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T z))$
179	177 178	sylib	$⊢ \exists b \in s [\{a\}] \forall w \in s \neg w T ⟨a, b⟩ \to \exists z \exists b (z = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T z))$
180		df-rex	$⊢ \exists z \in ({s ↾}_{\{a\}}) \forall w \in s \neg w T z \leftrightarrow \exists z (z \in ({s ↾}_{\{a\}}) \land \forall w \in s \neg w T z)$
181	56	elsnres	$⊢ z \in ({s ↾}_{\{a\}}) \leftrightarrow \exists b (z = ⟨a, b⟩ \land ⟨a, b⟩ \in s)$
182	181	anbi1i	$⊢ (z \in ({s ↾}_{\{a\}}) \land \forall w \in s \neg w T z) \leftrightarrow (\exists b (z = ⟨a, b⟩ \land ⟨a, b⟩ \in s) \land \forall w \in s \neg w T z)$
183		19.41v	$⊢ \exists b ((z = ⟨a, b⟩ \land ⟨a, b⟩ \in s) \land \forall w \in s \neg w T z) \leftrightarrow (\exists b (z = ⟨a, b⟩ \land ⟨a, b⟩ \in s) \land \forall w \in s \neg w T z)$
184		anass	$⊢ ((z = ⟨a, b⟩ \land ⟨a, b⟩ \in s) \land \forall w \in s \neg w T z) \leftrightarrow (z = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T z))$
185	184	exbii	$⊢ \exists b ((z = ⟨a, b⟩ \land ⟨a, b⟩ \in s) \land \forall w \in s \neg w T z) \leftrightarrow \exists b (z = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T z))$
186	182 183 185	3bitr2i	$⊢ (z \in ({s ↾}_{\{a\}}) \land \forall w \in s \neg w T z) \leftrightarrow \exists b (z = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T z))$
187	186	exbii	$⊢ \exists z (z \in ({s ↾}_{\{a\}}) \land \forall w \in s \neg w T z) \leftrightarrow \exists z \exists b (z = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T z))$
188	180 187	bitri	$⊢ \exists z \in ({s ↾}_{\{a\}}) \forall w \in s \neg w T z \leftrightarrow \exists z \exists b (z = ⟨a, b⟩ \land (⟨a, b⟩ \in s \land \forall w \in s \neg w T z))$
189	179 188	sylibr	$⊢ \exists b \in s [\{a\}] \forall w \in s \neg w T ⟨a, b⟩ \to \exists z \in ({s ↾}_{\{a\}}) \forall w \in s \neg w T z$
190		ssrexv	$⊢ {s ↾}_{\{a\}} \subseteq s \to (\exists z \in ({s ↾}_{\{a\}}) \forall w \in s \neg w T z \to \exists z \in s \forall w \in s \neg w T z)$
191	164 189 190	mpsyl	$⊢ \exists b \in s [\{a\}] \forall w \in s \neg w T ⟨a, b⟩ \to \exists z \in s \forall w \in s \neg w T z$
192	163 191	syl6	$⊢ (S Fr B \land s \subseteq A \times B \land s \neq \emptyset) \to ((a \in dom s \land \forall c \in dom s \neg c R a) \to \exists z \in s \forall w \in s \neg w T z)$
193	192	expd	$⊢ (S Fr B \land s \subseteq A \times B \land s \neq \emptyset) \to (a \in dom s \to (\forall c \in dom s \neg c R a \to \exists z \in s \forall w \in s \neg w T z))$
194	193	rexlimdv	$⊢ (S Fr B \land s \subseteq A \times B \land s \neq \emptyset) \to (\exists a \in dom s \forall c \in dom s \neg c R a \to \exists z \in s \forall w \in s \neg w T z)$
195	194	3expib	$⊢ S Fr B \to ((s \subseteq A \times B \land s \neq \emptyset) \to (\exists a \in dom s \forall c \in dom s \neg c R a \to \exists z \in s \forall w \in s \neg w T z))$
196	195	adantl	$⊢ (R Fr A \land S Fr B) \to ((s \subseteq A \times B \land s \neq \emptyset) \to (\exists a \in dom s \forall c \in dom s \neg c R a \to \exists z \in s \forall w \in s \neg w T z))$
197	34 196	mpdd	$⊢ (R Fr A \land S Fr B) \to ((s \subseteq A \times B \land s \neq \emptyset) \to \exists z \in s \forall w \in s \neg w T z)$
198	197	alrimiv	$⊢ (R Fr A \land S Fr B) \to \forall s ((s \subseteq A \times B \land s \neq \emptyset) \to \exists z \in s \forall w \in s \neg w T z)$
199		df-fr	$⊢ T Fr (A \times B) \leftrightarrow \forall s ((s \subseteq A \times B \land s \neq \emptyset) \to \exists z \in s \forall w \in s \neg w T z)$
200	198 199	sylibr	$⊢ (R Fr A \land S Fr B) \to T Fr (A \times B)$

Metamath Proof Explorer

Theorem frxp

Proof