Theorem frxp 13951

Description: A lexicographical ordering of two well founded classes.

Hypotheses

Ref	Expression
frxp.1	|- R Fr A
frxp.2	|- S Fr B
frxp.3	|- T = {<.x, y>. | ((x e. (A X. B) /\ y e. (A X. B)) /\ ((1st` x)R(1st` y) \/ ((1st` x) = (1st` y) /\ (2nd` x)S(2nd` y))))}

Assertion

Ref	Expression
frxp	|- T Fr (A X. B)

Distinct variable groups:   x,A,y   x,B,y   x,R,y   x,S,y

Proof of Theorem frxp

Step	Hyp	Ref	Expression
1		df-fr 3625	. 2 |- (T Fr (A X. B) <-> A.s((s C_ (A X. B) /\ s =/= (/)) -> E.z e. s A.w e. s -. wTz))
2		xpeq0 4336	. . . . . . . 8 |- ((A X. B) = (/) <-> (A = (/) \/ B = (/)))
3	2	biimpri 169	. . . . . . 7 |- ((A = (/) \/ B = (/)) -> (A X. B) = (/))
4	3	olcs 297	. . . . . 6 |- (B = (/) -> (A X. B) = (/))
5		sseq2 2639	. . . . . . 7 |- ((A X. B) = (/) -> (s C_ (A X. B) <-> s C_ (/)))
6		ss0 2902	. . . . . . . 8 |- (s C_ (/) -> s = (/))
7		dm0 4170	. . . . . . . . . 10 |- dom (/) = (/)
8		0ss 2900	. . . . . . . . . 10 |- (/) C_ A
9	7, 8	eqsstri 2647	. . . . . . . . 9 |- dom (/) C_ A
10		dmeq 4157	. . . . . . . . . 10 |- (s = (/) -> dom s = dom (/))
11	10	sseq1d 2644	. . . . . . . . 9 |- (s = (/) -> (dom s C_ A <-> dom (/) C_ A))
12	9, 11	mpbiri 211	. . . . . . . 8 |- (s = (/) -> dom s C_ A)
13	6, 12	syl 12	. . . . . . 7 |- (s C_ (/) -> dom s C_ A)
14	5, 13	syl6bi 231	. . . . . 6 |- ((A X. B) = (/) -> (s C_ (A X. B) -> dom s C_ A))
15	4, 14	syl 12	. . . . 5 |- (B = (/) -> (s C_ (A X. B) -> dom s C_ A))
16		dmxp 4177	. . . . . 6 |- (B =/= (/) -> dom ( A X. B) = A)
17		sseq2 2639	. . . . . . 7 |- (dom ( A X. B) = A -> (dom s C_ dom ( A X. B) <-> dom s C_ A))
18		dmss 4156	. . . . . . 7 |- (s C_ (A X. B) -> dom s C_ dom ( A X. B))
19	17, 18	syl5bi 225	. . . . . 6 |- (dom ( A X. B) = A -> (s C_ (A X. B) -> dom s C_ A))
20	16, 19	syl 12	. . . . 5 |- (B =/= (/) -> (s C_ (A X. B) -> dom s C_ A))
21	15, 20	pm2.61ine 2089	. . . 4 |- (s C_ (A X. B) -> dom s C_ A)
22	21	adantr 425	. . 3 |- ((s C_ (A X. B) /\ s =/= (/)) -> dom s C_ A)
23		relxp 4088	. . . . . . 7 |- Rel (A X. B)
24		relss 4074	. . . . . . 7 |- (s C_ (A X. B) -> (Rel (A X. B) -> Rel s))
25	23, 24	mpi 55	. . . . . 6 |- (s C_ (A X. B) -> Rel s)
26		reldm0 4176	. . . . . 6 |- (Rel s -> (s = (/) <-> dom s = (/)))
27	25, 26	syl 12	. . . . 5 |- (s C_ (A X. B) -> (s = (/) <-> dom s = (/)))
28	27	necon3bid 2035	. . . 4 |- (s C_ (A X. B) -> (s =/= (/) <-> dom s =/= (/)))
29	28	biimpa 460	. . 3 |- ((s C_ (A X. B) /\ s =/= (/)) -> dom s =/= (/))
30		visset 2295	. . . . . . . . . . . . 13 |- s e. _V
31		imaexg 4279	. . . . . . . . . . . . 13 |- (s e. _V -> (s"{a}) e. _V)
32	30, 31	ax-mp 7	. . . . . . . . . . . 12 |- (s"{a}) e. _V
33		sseq1 2637	. . . . . . . . . . . . . 14 |- (v = (s"{a}) -> (v C_ B <-> (s"{a}) C_ B))
34		neeq1 2024	. . . . . . . . . . . . . 14 |- (v = (s"{a}) -> (v =/= (/) <-> (s"{a}) =/= (/)))
35	33, 34	anbi12d 690	. . . . . . . . . . . . 13 |- (v = (s"{a}) -> ((v C_ B /\ v =/= (/)) <-> ((s"{a}) C_ B /\ (s"{a}) =/= (/))))
36		raleq 2266	. . . . . . . . . . . . . 14 |- (v = (s"{a}) -> (A.d e. v -. dSb <-> A.d e. (s"{a}) -. dSb))
37	36	rexeqbi1dv 2272	. . . . . . . . . . . . 13 |- (v = (s"{a}) -> (E.b e. v A.d e. v -. dSb <-> E.b e. (s"{a})A.d e. (s"{a}) -. dSb))
38	35, 37	imbi12d 688	. . . . . . . . . . . 12 |- (v = (s"{a}) -> (((v C_ B /\ v =/= (/)) -> E.b e. v A.d e. v -. dSb) <-> (((s"{a}) C_ B /\ (s"{a}) =/= (/)) -> E.b e. (s"{a})A.d e. (s"{a}) -. dSb)))
39		frxp.2	. . . . . . . . . . . . . 14 |- S Fr B
40		df-fr 3625	. . . . . . . . . . . . . 14 |- (S Fr B <-> A.v((v C_ B /\ v =/= (/)) -> E.b e. v A.d e. v -. dSb))
41	39, 40	mpbi 206	. . . . . . . . . . . . 13 |- A.v((v C_ B /\ v =/= (/)) -> E.b e. v A.d e. v -. dSb)
42	41	a4i 1328	. . . . . . . . . . . 12 |- ((v C_ B /\ v =/= (/)) -> E.b e. v A.d e. v -. dSb)
43	32, 38, 42	vtocl 2339	. . . . . . . . . . 11 |- (((s"{a}) C_ B /\ (s"{a}) =/= (/)) -> E.b e. (s"{a})A.d e. (s"{a}) -. dSb)
44		sstr 2625	. . . . . . . . . . . 12 |- (((s"{a}) C_ ran s /\ ran s C_ B) -> (s"{a}) C_ B)
45		imassrn 4278	. . . . . . . . . . . 12 |- (s"{a}) C_ ran s
46	3	orcs 296	. . . . . . . . . . . . . 14 |- (A = (/) -> (A X. B) = (/))
47		rn0 4203	. . . . . . . . . . . . . . . . . 18 |- ran (/) = (/)
48		0ss 2900	. . . . . . . . . . . . . . . . . 18 |- (/) C_ B
49	47, 48	eqsstri 2647	. . . . . . . . . . . . . . . . 17 |- ran (/) C_ B
50		rneq 4186	. . . . . . . . . . . . . . . . . 18 |- (s = (/) -> ran s = ran (/))
51	50	sseq1d 2644	. . . . . . . . . . . . . . . . 17 |- (s = (/) -> (ran s C_ B <-> ran (/) C_ B))
52	49, 51	mpbiri 211	. . . . . . . . . . . . . . . 16 |- (s = (/) -> ran s C_ B)
53	6, 52	syl 12	. . . . . . . . . . . . . . 15 |- (s C_ (/) -> ran s C_ B)
54	5, 53	syl6bi 231	. . . . . . . . . . . . . 14 |- ((A X. B) = (/) -> (s C_ (A X. B) -> ran s C_ B))
55	46, 54	syl 12	. . . . . . . . . . . . 13 |- (A = (/) -> (s C_ (A X. B) -> ran s C_ B))
56		rnxp 4342	. . . . . . . . . . . . . 14 |- (A =/= (/) -> ran ( A X. B) = B)
57		sseq2 2639	. . . . . . . . . . . . . . 15 |- (ran ( A X. B) = B -> (ran s C_ ran ( A X. B) <-> ran s C_ B))
58		rnss 4189	. . . . . . . . . . . . . . 15 |- (s C_ (A X. B) -> ran s C_ ran ( A X. B))
59	57, 58	syl5bi 225	. . . . . . . . . . . . . 14 |- (ran ( A X. B) = B -> (s C_ (A X. B) -> ran s C_ B))
60	56, 59	syl 12	. . . . . . . . . . . . 13 |- (A =/= (/) -> (s C_ (A X. B) -> ran s C_ B))
61	55, 60	pm2.61ine 2089	. . . . . . . . . . . 12 |- (s C_ (A X. B) -> ran s C_ B)
62	44, 45, 61	sylancr 526	. . . . . . . . . . 11 |- (s C_ (A X. B) -> (s"{a}) C_ B)
63		visset 2295	. . . . . . . . . . . . 13 |- a e. _V
64	63	eldm 4153	. . . . . . . . . . . 12 |- (a e. dom s <-> E.b asb)
65		visset 2295	. . . . . . . . . . . . . . . 16 |- b e. _V
66	63, 65	elimasn 4289	. . . . . . . . . . . . . . 15 |- (b e. (s"{a}) <-> <.a, b>. e. s)
67		df-br 3339	. . . . . . . . . . . . . . 15 |- (asb <-> <.a, b>. e. s)
68	66, 67	bitr4i 193	. . . . . . . . . . . . . 14 |- (b e. (s"{a}) <-> asb)
69		ne0i 2881	. . . . . . . . . . . . . 14 |- (b e. (s"{a}) -> (s"{a}) =/= (/))
70	68, 69	sylbir 218	. . . . . . . . . . . . 13 |- (asb -> (s"{a}) =/= (/))
71	70	19.23aiv 1674	. . . . . . . . . . . 12 |- (E.b asb -> (s"{a}) =/= (/))
72	64, 71	sylbi 216	. . . . . . . . . . 11 |- (a e. dom s -> (s"{a}) =/= (/))
73	43, 62, 72	syl2an 503	. . . . . . . . . 10 |- ((s C_ (A X. B) /\ a e. dom s) -> E.b e. (s"{a})A.d e. (s"{a}) -. dSb)
74		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (c = (1st` w) -> (cRa <-> (1st` w)Ra))
75	74	notbid 673	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (c = (1st` w) -> (-. cRa <-> -. (1st` w)Ra))
76	75	rcla4cv 2377	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.c e. dom s -. cRa -> ((1st` w) e. dom s -> -. (1st` w)Ra))
77		1stdm 5049	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((Rel s /\ w e. s) -> (1st` w) e. dom s)
78	76, 77	syl5 20	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A.c e. dom s -. cRa -> ((Rel s /\ w e. s) -> -. (1st` w)Ra))
79	78	exp3a 405	. . . . . . . . . . . . . . . . . . . . . 22 |- (A.c e. dom s -. cRa -> (Rel s -> (w e. s -> -. (1st` w)Ra)))
80	79	impcom 378	. . . . . . . . . . . . . . . . . . . . 21 |- ((Rel s /\ A.c e. dom s -. cRa) -> (w e. s -> -. (1st` w)Ra))
81	80	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- (((Rel s /\ A.c e. dom s -. cRa) /\ A.d e. (s"{a}) -. dSb) -> (w e. s -> -. (1st` w)Ra))
82		elrel 4086	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((Rel s /\ w e. s) -> E.tE.u w = <.t, u>.)
83	82	ex 402	. . . . . . . . . . . . . . . . . . . . . . 23 |- (Rel s -> (w e. s -> E.tE.u w = <.t, u>.))
84	83	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 |- ((Rel s /\ A.d e. (s"{a}) -. dSb) -> (w e. s -> E.tE.u w = <.t, u>.))
85		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = <.t, u>. -> (w e. s <-> <.t, u>. e. s))
86		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = <.t, u>. -> (1st` w) = (1st` <.t, u>.))
87		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- t e. _V
88	87	op1st 5026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (1st` <.t, u>.) = t
89	86, 88	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = <.t, u>. -> (1st` w) = t)
90	89	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = <.t, u>. -> ((1st` w) = a <-> t = a))
91		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w = <.t, u>. -> (2nd` w) = (2nd` <.t, u>.))
92		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- u e. _V
93	87, 92	op2nd 5027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (2nd` <.t, u>.) = u
94	91, 93	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = <.t, u>. -> (2nd` w) = u)
95	94	breq1d 3348	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = <.t, u>. -> ((2nd` w)Sb <-> uSb))
96	95	notbid 673	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = <.t, u>. -> (-. (2nd` w)Sb <-> -. uSb))
97	90, 96	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = <.t, u>. -> (((1st` w) = a -> -. (2nd` w)Sb) <-> (t = a -> -. uSb)))
98	85, 97	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = <.t, u>. -> ((w e. s -> ((1st` w) = a -> -. (2nd` w)Sb)) <-> (<.t, u>. e. s -> (t = a -> -. uSb))))
99		opeq1 3158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (t = a -> <.t, u>. = <.a, u>.)
100	99	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = a -> (<.t, u>. e. s <-> <.a, u>. e. s))
101	100	imbi1d 675	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (t = a -> ((<.t, u>. e. s -> -. uSb) <-> (<.a, u>. e. s -> -. uSb)))
102		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (d = u -> (dSb <-> uSb))
103	102	notbid 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (d = u -> (-. dSb <-> -. uSb))
104	103	rcla4cv 2377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (A.d e. (s"{a}) -. dSb -> (u e. (s"{a}) -> -. uSb))
105	63, 92	elimasn 4289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (u e. (s"{a}) <-> <.a, u>. e. s)
106	104, 105	syl5ibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (A.d e. (s"{a}) -. dSb -> (<.a, u>. e. s -> -. uSb))
107	106	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((Rel s /\ A.d e. (s"{a}) -. dSb) -> (<.a, u>. e. s -> -. uSb))
108	101, 107	syl5bir 227	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (t = a -> ((Rel s /\ A.d e. (s"{a}) -. dSb) -> (<.t, u>. e. s -> -. uSb)))
109	108	com3l 38	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((Rel s /\ A.d e. (s"{a}) -. dSb) -> (<.t, u>. e. s -> (t = a -> -. uSb)))
110	98, 109	syl5bir 227	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w = <.t, u>. -> ((Rel s /\ A.d e. (s"{a}) -. dSb) -> (w e. s -> ((1st` w) = a -> -. (2nd` w)Sb))))
111	110	19.23aivv 1675	. . . . . . . . . . . . . . . . . . . . . . 23 |- (E.tE.u w = <.t, u>. -> ((Rel s /\ A.d e. (s"{a}) -. dSb) -> (w e. s -> ((1st` w) = a -> -. (2nd` w)Sb))))
112	111	com3l 38	. . . . . . . . . . . . . . . . . . . . . 22 |- ((Rel s /\ A.d e. (s"{a}) -. dSb) -> (w e. s -> (E.tE.u w = <.t, u>. -> ((1st` w) = a -> -. (2nd` w)Sb))))
113	84, 112	mpdd 57	. . . . . . . . . . . . . . . . . . . . 21 |- ((Rel s /\ A.d e. (s"{a}) -. dSb) -> (w e. s -> ((1st` w) = a -> -. (2nd` w)Sb)))
114	113	adantlr 429	. . . . . . . . . . . . . . . . . . . 20 |- (((Rel s /\ A.c e. dom s -. cRa) /\ A.d e. (s"{a}) -. dSb) -> (w e. s -> ((1st` w) = a -> -. (2nd` w)Sb)))
115	81, 114	jcad 661	. . . . . . . . . . . . . . . . . . 19 |- (((Rel s /\ A.c e. dom s -. cRa) /\ A.d e. (s"{a}) -. dSb) -> (w e. s -> (-. (1st` w)Ra /\ ((1st` w) = a -> -. (2nd` w)Sb))))
116	115	r19.21aiv 2175	. . . . . . . . . . . . . . . . . 18 |- (((Rel s /\ A.c e. dom s -. cRa) /\ A.d e. (s"{a}) -. dSb) -> A.w e. s (-. (1st` w)Ra /\ ((1st` w) = a -> -. (2nd` w)Sb)))
117	116	ex 402	. . . . . . . . . . . . . . . . 17 |- ((Rel s /\ A.c e. dom s -. cRa) -> (A.d e. (s"{a}) -. dSb -> A.w e. s (-. (1st` w)Ra /\ ((1st` w) = a -> -. (2nd` w)Sb))))
118	117, 25	sylan 497	. . . . . . . . . . . . . . . 16 |- ((s C_ (A X. B) /\ A.c e. dom s -. cRa) -> (A.d e. (s"{a}) -. dSb -> A.w e. s (-. (1st` w)Ra /\ ((1st` w) = a -> -. (2nd` w)Sb))))
119		olc 290	. . . . . . . . . . . . . . . . 17 |- ((-. (1st` w)Ra /\ ((1st` w) = a -> -. (2nd` w)Sb)) -> (-. (w e. (A X. B) /\ <.a, b>. e. (A X. B)) \/ (-. (1st` w)Ra /\ ((1st` w) = a -> -. (2nd` w)Sb))))
120	119	ralimi 2168	. . . . . . . . . . . . . . . 16 |- (A.w e. s (-. (1st` w)Ra /\ ((1st` w) = a -> -. (2nd` w)Sb)) -> A.w e. s (-. (w e. (A X. B) /\ <.a, b>. e. (A X. B)) \/ (-. (1st` w)Ra /\ ((1st` w) = a -> -. (2nd` w)Sb))))
121	118, 120	syl6 25	. . . . . . . . . . . . . . 15 |- ((s C_ (A X. B) /\ A.c e. dom s -. cRa) -> (A.d e. (s"{a}) -. dSb -> A.w e. s (-. (w e. (A X. B) /\ <.a, b>. e. (A X. B)) \/ (-. (1st` w)Ra /\ ((1st` w) = a -> -. (2nd` w)Sb)))))
122		visset 2295	. . . . . . . . . . . . . . . . . . 19 |- w e. _V
123		opex 3527	. . . . . . . . . . . . . . . . . . 19 |- <.a, b>. e. _V
124		eleq1 1957	. . . . . . . . . . . . . . . . . . . . 21 |- (x = w -> (x e. (A X. B) <-> w e. (A X. B)))
125	124	anbi1d 679	. . . . . . . . . . . . . . . . . . . 20 |- (x = w -> ((x e. (A X. B) /\ y e. (A X. B)) <-> (w e. (A X. B) /\ y e. (A X. B))))
126		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = w -> (1st` x) = (1st` w))
127	126	breq1d 3348	. . . . . . . . . . . . . . . . . . . . 21 |- (x = w -> ((1st` x)R(1st` y) <-> (1st` w)R(1st` y)))
128	126	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = w -> ((1st` x) = (1st` y) <-> (1st` w) = (1st` y)))
129		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = w -> (2nd` x) = (2nd` w))
130	129	breq1d 3348	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = w -> ((2nd` x)S(2nd` y) <-> (2nd` w)S(2nd` y)))
131	128, 130	anbi12d 690	. . . . . . . . . . . . . . . . . . . . 21 |- (x = w -> (((1st` x) = (1st` y) /\ (2nd` x)S(2nd` y)) <-> ((1st` w) = (1st` y) /\ (2nd` w)S(2nd` y))))
132	127, 131	orbi12d 689	. . . . . . . . . . . . . . . . . . . 20 |- (x = w -> (((1st` x)R(1st` y) \/ ((1st` x) = (1st` y) /\ (2nd` x)S(2nd` y))) <-> ((1st` w)R(1st` y) \/ ((1st` w) = (1st` y) /\ (2nd` w)S(2nd` y)))))
133	125, 132	anbi12d 690	. . . . . . . . . . . . . . . . . . 19 |- (x = w -> (((x e. (A X. B) /\ y e. (A X. B)) /\ ((1st` x)R(1st` y) \/ ((1st` x) = (1st` y) /\ (2nd` x)S(2nd` y)))) <-> ((w e. (A X. B) /\ y e. (A X. B)) /\ ((1st` w)R(1st` y) \/ ((1st` w) = (1st` y) /\ (2nd` w)S(2nd` y))))))
134		eleq1 1957	. . . . . . . . . . . . . . . . . . . . 21 |- (y = <.a, b>. -> (y e. (A X. B) <-> <.a, b>. e. (A X. B)))
135	134	anbi2d 678	. . . . . . . . . . . . . . . . . . . 20 |- (y = <.a, b>. -> ((w e. (A X. B) /\ y e. (A X. B)) <-> (w e. (A X. B) /\ <.a, b>. e. (A X. B))))
136		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = <.a, b>. -> (1st` y) = (1st` <.a, b>.))
137	63	op1st 5026	. . . . . . . . . . . . . . . . . . . . . . 23 |- (1st` <.a, b>.) = a
138	136, 137	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = <.a, b>. -> (1st` y) = a)
139	138	breq2d 3350	. . . . . . . . . . . . . . . . . . . . 21 |- (y = <.a, b>. -> ((1st` w)R(1st` y) <-> (1st` w)Ra))
140	138	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = <.a, b>. -> ((1st` w) = (1st` y) <-> (1st` w) = a))
141		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y = <.a, b>. -> (2nd` y) = (2nd` <.a, b>.))
142	63, 65	op2nd 5027	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (2nd` <.a, b>.) = b
143	141, 142	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = <.a, b>. -> (2nd` y) = b)
144	143	breq2d 3350	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = <.a, b>. -> ((2nd` w)S(2nd` y) <-> (2nd` w)Sb))
145	140, 144	anbi12d 690	. . . . . . . . . . . . . . . . . . . . 21 |- (y = <.a, b>. -> (((1st` w) = (1st` y) /\ (2nd` w)S(2nd` y)) <-> ((1st` w) = a /\ (2nd` w)Sb)))
146	139, 145	orbi12d 689	. . . . . . . . . . . . . . . . . . . 20 |- (y = <.a, b>. -> (((1st` w)R(1st` y) \/ ((1st` w) = (1st` y) /\ (2nd` w)S(2nd` y))) <-> ((1st` w)Ra \/ ((1st` w) = a /\ (2nd` w)Sb))))
147	135, 146	anbi12d 690	. . . . . . . . . . . . . . . . . . 19 |- (y = <.a, b>. -> (((w e. (A X. B) /\ y e. (A X. B)) /\ ((1st` w)R(1st` y) \/ ((1st` w) = (1st` y) /\ (2nd` w)S(2nd` y)))) <-> ((w e. (A X. B) /\ <.a, b>. e. (A X. B)) /\ ((1st` w)Ra \/ ((1st` w) = a /\ (2nd` w)Sb)))))
148		frxp.3	. . . . . . . . . . . . . . . . . . 19 |- T = {<.x, y>. | ((x e. (A X. B) /\ y e. (A X. B)) /\ ((1st` x)R(1st` y) \/ ((1st` x) = (1st` y) /\ (2nd` x)S(2nd` y))))}
149	122, 123, 133, 147, 148	brab 3571	. . . . . . . . . . . . . . . . . 18 |- (wT<.a, b>. <-> ((w e. (A X. B) /\ <.a, b>. e. (A X. B)) /\ ((1st` w)Ra \/ ((1st` w) = a /\ (2nd` w)Sb))))
150	149	notbii 204	. . . . . . . . . . . . . . . . 17 |- (-. wT<.a, b>. <-> -. ((w e. (A X. B) /\ <.a, b>. e. (A X. B)) /\ ((1st` w)Ra \/ ((1st` w) = a /\ (2nd` w)Sb))))
151		ianor 329	. . . . . . . . . . . . . . . . 17 |- (-. ((w e. (A X. B) /\ <.a, b>. e. (A X. B)) /\ ((1st` w)Ra \/ ((1st` w) = a /\ (2nd` w)Sb))) <-> (-. (w e. (A X. B) /\ <.a, b>. e. (A X. B)) \/ -. ((1st` w)Ra \/ ((1st` w) = a /\ (2nd` w)Sb))))
152		ioran 331	. . . . . . . . . . . . . . . . . . 19 |- (-. ((1st` w)Ra \/ ((1st` w) = a /\ (2nd` w)Sb)) <-> (-. (1st` w)Ra /\ -. ((1st` w) = a /\ (2nd` w)Sb)))
153		ianor 329	. . . . . . . . . . . . . . . . . . . . 21 |- (-. ((1st` w) = a /\ (2nd` w)Sb) <-> (-. (1st` w) = a \/ -. (2nd` w)Sb))
154		pm4.62 254	. . . . . . . . . . . . . . . . . . . . 21 |- (((1st` w) = a -> -. (2nd` w)Sb) <-> (-. (1st` w) = a \/ -. (2nd` w)Sb))
155	153, 154	bitr4i 193	. . . . . . . . . . . . . . . . . . . 20 |- (-. ((1st` w) = a /\ (2nd` w)Sb) <-> ((1st` w) = a -> -. (2nd` w)Sb))
156	155	anbi2i 538	. . . . . . . . . . . . . . . . . . 19 |- ((-. (1st` w)Ra /\ -. ((1st` w) = a /\ (2nd` w)Sb)) <-> (-. (1st` w)Ra /\ ((1st` w) = a -> -. (2nd` w)Sb)))
157	152, 156	bitri 190	. . . . . . . . . . . . . . . . . 18 |- (-. ((1st` w)Ra \/ ((1st` w) = a /\ (2nd` w)Sb)) <-> (-. (1st` w)Ra /\ ((1st` w) = a -> -. (2nd` w)Sb)))
158	157	orbi2i 275	. . . . . . . . . . . . . . . . 17 |- ((-. (w e. (A X. B) /\ <.a, b>. e. (A X. B)) \/ -. ((1st` w)Ra \/ ((1st` w) = a /\ (2nd` w)Sb))) <-> (-. (w e. (A X. B) /\ <.a, b>. e. (A X. B)) \/ (-. (1st` w)Ra /\ ((1st` w) = a -> -. (2nd` w)Sb))))
159	150, 151, 158	3bitri 194	. . . . . . . . . . . . . . . 16 |- (-. wT<.a, b>. <-> (-. (w e. (A X. B) /\ <.a, b>. e. (A X. B)) \/ (-. (1st` w)Ra /\ ((1st` w) = a -> -. (2nd` w)Sb))))
160	159	ralbii 2127	. . . . . . . . . . . . . . 15 |- (A.w e. s -. wT<.a, b>. <-> A.w e. s (-. (w e. (A X. B) /\ <.a, b>. e. (A X. B)) \/ (-. (1st` w)Ra /\ ((1st` w) = a -> -. (2nd` w)Sb))))
161	121, 160	syl6ibr 230	. . . . . . . . . . . . . 14 |- ((s C_ (A X. B) /\ A.c e. dom s -. cRa) -> (A.d e. (s"{a}) -. dSb -> A.w e. s -. wT<.a, b>.))
162	161	reximdv 2202	. . . . . . . . . . . . 13 |- ((s C_ (A X. B) /\ A.c e. dom s -. cRa) -> (E.b e. (s"{a})A.d e. (s"{a}) -. dSb -> E.b e. (s"{a})A.w e. s -. wT<.a, b>.))
163	162	ex 402	. . . . . . . . . . . 12 |- (s C_ (A X. B) -> (A.c e. dom s -. cRa -> (E.b e. (s"{a})A.d e. (s"{a}) -. dSb -> E.b e. (s"{a})A.w e. s -. wT<.a, b>.)))
164	163	com23 36	. . . . . . . . . . 11 |- (s C_ (A X. B) -> (E.b e. (s"{a})A.d e. (s"{a}) -. dSb -> (A.c e. dom s -. cRa -> E.b e. (s"{a})A.w e. s -. wT<.a, b>.)))
165	164	adantr 425	. . . . . . . . . 10 |- ((s C_ (A X. B) /\ a e. dom s) -> (E.b e. (s"{a})A.d e. (s"{a}) -. dSb -> (A.c e. dom s -. cRa -> E.b e. (s"{a})A.w e. s -. wT<.a, b>.)))
166	73, 165	mpd 29	. . . . . . . . 9 |- ((s C_ (A X. B) /\ a e. dom s) -> (A.c e. dom s -. cRa -> E.b e. (s"{a})A.w e. s -. wT<.a, b>.))
167	166	expimpd 404	. . . . . . . 8 |- (s C_ (A X. B) -> ((a e. dom s /\ A.c e. dom s -. cRa) -> E.b e. (s"{a})A.w e. s -. wT<.a, b>.))
168	167	adantr 425	. . . . . . 7 |- ((s C_ (A X. B) /\ s =/= (/)) -> ((a e. dom s /\ A.c e. dom s -. cRa) -> E.b e. (s"{a})A.w e. s -. wT<.a, b>.))
169		df-rex 2110	. . . . . . . . . . 11 |- (E.b e. (s"{a})A.w e. s -. wT<.a, b>. <-> E.b(b e. (s"{a}) /\ A.w e. s -. wT<.a, b>.))
170		eqid 1884	. . . . . . . . . . . . . 14 |- <.a, b>. = <.a, b>.
171		eqeq1 1890	. . . . . . . . . . . . . . . 16 |- (z = <.a, b>. -> (z = <.a, b>. <-> <.a, b>. = <.a, b>.))
172		breq2 3342	. . . . . . . . . . . . . . . . . . 19 |- (z = <.a, b>. -> (wTz <-> wT<.a, b>.))
173	172	notbid 673	. . . . . . . . . . . . . . . . . 18 |- (z = <.a, b>. -> (-. wTz <-> -. wT<.a, b>.))
174	173	ralbidv 2123	. . . . . . . . . . . . . . . . 17 |- (z = <.a, b>. -> (A.w e. s -. wTz <-> A.w e. s -. wT<.a, b>.))
175	174	anbi2d 678	. . . . . . . . . . . . . . . 16 |- (z = <.a, b>. -> ((<.a, b>. e. s /\ A.w e. s -. wTz) <-> (<.a, b>. e. s /\ A.w e. s -. wT<.a, b>.)))
176	171, 175	anbi12d 690	. . . . . . . . . . . . . . 15 |- (z = <.a, b>. -> ((z = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wTz)) <-> (<.a, b>. = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wT<.a, b>.))))
177	123, 176	cla4ev 2371	. . . . . . . . . . . . . 14 |- ((<.a, b>. = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wT<.a, b>.)) -> E.z(z = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wTz)))
178	170, 177	mpan 759	. . . . . . . . . . . . 13 |- ((<.a, b>. e. s /\ A.w e. s -. wT<.a, b>.) -> E.z(z = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wTz)))
179	178, 66	sylanb 498	. . . . . . . . . . . 12 |- ((b e. (s"{a}) /\ A.w e. s -. wT<.a, b>.) -> E.z(z = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wTz)))
180	179	eximi 1387	. . . . . . . . . . 11 |- (E.b(b e. (s"{a}) /\ A.w e. s -. wT<.a, b>.) -> E.bE.z(z = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wTz)))
181	169, 180	sylbi 216	. . . . . . . . . 10 |- (E.b e. (s"{a})A.w e. s -. wT<.a, b>. -> E.bE.z(z = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wTz)))
182		excom 1393	. . . . . . . . . 10 |- (E.bE.z(z = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wTz)) <-> E.zE.b(z = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wTz)))
183	181, 182	sylib 215	. . . . . . . . 9 |- (E.b e. (s"{a})A.w e. s -. wT<.a, b>. -> E.zE.b(z = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wTz)))
184		df-rex 2110	. . . . . . . . . 10 |- (E.z e. (s |` {a})A.w e. s -. wTz <-> E.z(z e. (s |` {a}) /\ A.w e. s -. wTz))
185	63	elsnres 13825	. . . . . . . . . . . . 13 |- (z e. (s |` {a}) <-> E.b(z = <.a, b>. /\ <.a, b>. e. s))
186	185	anbi1i 539	. . . . . . . . . . . 12 |- ((z e. (s |` {a}) /\ A.w e. s -. wTz) <-> (E.b(z = <.a, b>. /\ <.a, b>. e. s) /\ A.w e. s -. wTz))
187		19.41v 1685	. . . . . . . . . . . 12 |- (E.b((z = <.a, b>. /\ <.a, b>. e. s) /\ A.w e. s -. wTz) <-> (E.b(z = <.a, b>. /\ <.a, b>. e. s) /\ A.w e. s -. wTz))
188		anass 487	. . . . . . . . . . . . 13 |- (((z = <.a, b>. /\ <.a, b>. e. s) /\ A.w e. s -. wTz) <-> (z = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wTz)))
189	188	exbii 1398	. . . . . . . . . . . 12 |- (E.b((z = <.a, b>. /\ <.a, b>. e. s) /\ A.w e. s -. wTz) <-> E.b(z = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wTz)))
190	186, 187, 189	3bitr2i 196	. . . . . . . . . . 11 |- ((z e. (s |` {a}) /\ A.w e. s -. wTz) <-> E.b(z = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wTz)))
191	190	exbii 1398	. . . . . . . . . 10 |- (E.z(z e. (s |` {a}) /\ A.w e. s -. wTz) <-> E.zE.b(z = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wTz)))
192	184, 191	bitri 190	. . . . . . . . 9 |- (E.z e. (s |` {a})A.w e. s -. wTz <-> E.zE.b(z = <.a, b>. /\ (<.a, b>. e. s /\ A.w e. s -. wTz)))
193	183, 192	sylibr 217	. . . . . . . 8 |- (E.b e. (s"{a})A.w e. s -. wT<.a, b>. -> E.z e. (s |` {a})A.w e. s -. wTz)
194		resss 4237	. . . . . . . . 9 |- (s |` {a}) C_ s
195		ssrexv 2673	. . . . . . . . 9 |- ((s |` {a}) C_ s -> (E.z e. (s |` {a})A.w e. s -. wTz -> E.z e. s A.w e. s -. wTz))
196	194, 195	ax-mp 7	. . . . . . . 8 |- (E.z e. (s |` {a})A.w e. s -. wTz -> E.z e. s A.w e. s -. wTz)
197	193, 196	syl 12	. . . . . . 7 |- (E.b e. (s"{a})A.w e. s -. wT<.a, b>. -> E.z e. s A.w e. s -. wTz)
198	168, 197	syl6 25	. . . . . 6 |- ((s C_ (A X. B) /\ s =/= (/)) -> ((a e. dom s /\ A.c e. dom s -. cRa) -> E.z e. s A.w e. s -. wTz))
199	198	exp3a 405	. . . . 5 |- ((s C_ (A X. B) /\ s =/= (/)) -> (a e. dom s -> (A.c e. dom s -. cRa -> E.z e. s A.w e. s -. wTz)))
200	199	r19.23adv 2215	. . . 4 |- ((s C_ (A X. B) /\ s =/= (/)) -> (E.a e. dom sA.c e. dom s -. cRa -> E.z e. s A.w e. s -. wTz))
201	30	dmex 4208	. . . . 5 |- dom s e. _V
202		sseq1 2637	. . . . . . 7 |- (v = dom s -> (v C_ A <-> dom s C_ A))
203		neeq1 2024	. . . . . . 7 |- (v = dom s -> (v =/= (/) <-> dom s =/= (/)))
204	202, 203	anbi12d 690	. . . . . 6 |- (v = dom s -> ((v C_ A /\ v =/= (/)) <-> (dom s C_ A /\ dom s =/= (/))))
205		raleq 2266	. . . . . . 7 |- (v = dom s -> (A.c e. v -. cRa <-> A.c e. dom s -. cRa))
206	205	rexeqbi1dv 2272	. . . . . 6 |- (v = dom s -> (E.a e. v A.c e. v -. cRa <-> E.a e. dom sA.c e. dom s -. cRa))
207	204, 206	imbi12d 688	. . . . 5 |- (v = dom s -> (((v C_ A /\ v =/= (/)) -> E.a e. v A.c e. v -. cRa) <-> ((dom s C_ A /\ dom s =/= (/)) -> E.a e. dom sA.c e. dom s -. cRa)))
208		frxp.1	. . . . . . 7 |- R Fr A
209		df-fr 3625	. . . . . . 7 |- (R Fr A <-> A.v((v C_ A /\ v =/= (/)) -> E.a e. v A.c e. v -. cRa))
210	208, 209	mpbi 206	. . . . . 6 |- A.v((v C_ A /\ v =/= (/)) -> E.a e. v A.c e. v -. cRa)
211	210	a4i 1328	. . . . 5 |- ((v C_ A /\ v =/= (/)) -> E.a e. v A.c e. v -. cRa)
212	201, 207, 211	vtocl 2339	. . . 4 |- ((dom s C_ A /\ dom s =/= (/)) -> E.a e. dom sA.c e. dom s -. cRa)
213	200, 212	syl5 20	. . 3 |- ((s C_ (A X. B) /\ s =/= (/)) -> ((dom s C_ A /\ dom s =/= (/)) -> E.z e. s A.w e. s -. wTz))
214	22, 29, 213	mp2and 767	. 2 |- ((s C_ (A X. B) /\ s =/= (/)) -> E.z e. s A.w e. s -. wTz)
215	1, 214	mpgbir 1334	1 |- T Fr (A X. B)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593  (/)c0 2875  {csn 3044  <.cop 3046   class class class wbr 3338  {copab 3395   Fr wfr 3623   X. cxp 3984  dom cdm 3986  ran crn 3987   |` cres 3988  "cima 3989  Rel wrel 3991  ` cfv 3998  1stc1st 5018  2ndc2nd 5019

This theorem is referenced by:  wexp 13952

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-int 3215  df-br 3339  df-opab 3396  df-id 3586  df-fr 3625  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fv 4014  df-1st 5020  df-2nd 5021

Copyright terms: Public domain