Theorem fictblem 15370

Description: Lemma for fictb 15371.

Assertion

Ref	Expression
fictblem	|- (((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) -> (n C_ m -> ((r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)) -> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))))

Distinct variable groups:   m,n,r,s,u,v,w,x,y,z,A   B,m,n,r,s,u,v,w,x,y,z

Proof of Theorem fictblem

Step	Hyp	Ref	Expression
1		fveq2 4681	. . . . . . . 8 |- (x = n -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n))
2	1	sseq2d 2645	. . . . . . 7 |- (x = n -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) <-> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)))
3		fveq2 4681	. . . . . . . 8 |- (x = k -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k))
4	3	sseq2d 2645	. . . . . . 7 |- (x = k -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) <-> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)))
5		fveq2 4681	. . . . . . . 8 |- (x = suc k -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k))
6	5	sseq2d 2645	. . . . . . 7 |- (x = suc k -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) <-> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k)))
7		fveq2 4681	. . . . . . . 8 |- (x = m -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m))
8	7	sseq2d 2645	. . . . . . 7 |- (x = m -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) <-> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))
9		ssid 2634	. . . . . . . 8 |- (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)
10	9	a1i 8	. . . . . . 7 |- (n e. om -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n))
11		id 73	. . . . . . . . . . . . 13 |- (t e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) -> t e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k))
12		inidm 2803	. . . . . . . . . . . . . . 15 |- (t i^i t) = t
13	12	eqcomi 1888	. . . . . . . . . . . . . 14 |- t = (t i^i t)
14	13	a1i 8	. . . . . . . . . . . . 13 |- (t e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) -> t = (t i^i t))
15		ineq1 2789	. . . . . . . . . . . . . . 15 |- (m = t -> (m i^i n) = (t i^i n))
16	15	eqeq2d 1895	. . . . . . . . . . . . . 14 |- (m = t -> (t = (m i^i n) <-> t = (t i^i n)))
17		ineq2 2790	. . . . . . . . . . . . . . 15 |- (n = t -> (t i^i n) = (t i^i t))
18	17	eqeq2d 1895	. . . . . . . . . . . . . 14 |- (n = t -> (t = (t i^i n) <-> t = (t i^i t)))
19	16, 18	rcla42ev 2385	. . . . . . . . . . . . 13 |- ((t e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ t e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ t = (t i^i t)) -> E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)t = (m i^i n))
20	11, 14, 19	mpd3an23 1193	. . . . . . . . . . . 12 |- (t e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) -> E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)t = (m i^i n))
21		visset 2295	. . . . . . . . . . . . 13 |- t e. _V
22		eqeq1 1890	. . . . . . . . . . . . . 14 |- (c = t -> (c = (m i^i n) <-> t = (m i^i n)))
23	22	2rexbidv 2141	. . . . . . . . . . . . 13 |- (c = t -> (E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n) <-> E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)t = (m i^i n)))
24	21, 23	elab 2403	. . . . . . . . . . . 12 |- (t e. {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)} <-> E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)t = (m i^i n))
25	20, 24	sylibr 217	. . . . . . . . . . 11 |- (t e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) -> t e. {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)})
26	25	ssriv 2621	. . . . . . . . . 10 |- (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) C_ {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)}
27	26	a1i 8	. . . . . . . . 9 |- (((k e. om /\ n e. om) /\ n C_ k) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) C_ {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)})
28		nnon 3957	. . . . . . . . . . . 12 |- (k e. om -> k e. On)
29		rdgsuc 5153	. . . . . . . . . . . 12 |- (k e. On -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k) = ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)))
30	28, 29	syl 12	. . . . . . . . . . 11 |- (k e. om -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k) = ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)))
31	30	ad2antrr 440	. . . . . . . . . 10 |- (((k e. om /\ n e. om) /\ n C_ k) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k) = ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)))
32		rexeq 2267	. . . . . . . . . . . . . . . . . 18 |- (u = r -> (E.z e. u w = (y i^i z) <-> E.z e. r w = (y i^i z)))
33	32	rexeqbi1dv 2272	. . . . . . . . . . . . . . . . 17 |- (u = r -> (E.y e. u E.z e. u w = (y i^i z) <-> E.y e. r E.z e. r w = (y i^i z)))
34	33	abbidv 2008	. . . . . . . . . . . . . . . 16 |- (u = r -> {w | E.y e. u E.z e. u w = (y i^i z)} = {w | E.y e. r E.z e. r w = (y i^i z)})
35	34	eqeq2d 1895	. . . . . . . . . . . . . . 15 |- (u = r -> (v = {w | E.y e. u E.z e. u w = (y i^i z)} <-> v = {w | E.y e. r E.z e. r w = (y i^i z)}))
36		eqeq1 1890	. . . . . . . . . . . . . . 15 |- (v = s -> (v = {w | E.y e. r E.z e. r w = (y i^i z)} <-> s = {w | E.y e. r E.z e. r w = (y i^i z)}))
37	35, 36	sylan9bb 599	. . . . . . . . . . . . . 14 |- ((u = r /\ v = s) -> (v = {w | E.y e. u E.z e. u w = (y i^i z)} <-> s = {w | E.y e. r E.z e. r w = (y i^i z)}))
38	37	cbvopabv 3404	. . . . . . . . . . . . 13 |- {<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}} = {<.r, s>. | s = {w | E.y e. r E.z e. r w = (y i^i z)}}
39		eqeq1 1890	. . . . . . . . . . . . . . . . . 18 |- (w = c -> (w = (y i^i z) <-> c = (y i^i z)))
40	39	2rexbidv 2141	. . . . . . . . . . . . . . . . 17 |- (w = c -> (E.y e. r E.z e. r w = (y i^i z) <-> E.y e. r E.z e. r c = (y i^i z)))
41	40	cbvabv 2420	. . . . . . . . . . . . . . . 16 |- {w | E.y e. r E.z e. r w = (y i^i z)} = {c | E.y e. r E.z e. r c = (y i^i z)}
42		ineq1 2789	. . . . . . . . . . . . . . . . . . . . 21 |- (y = m -> (y i^i z) = (m i^i z))
43	42	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . 20 |- (y = m -> (c = (y i^i z) <-> c = (m i^i z)))
44	43	rexbidv 2124	. . . . . . . . . . . . . . . . . . 19 |- (y = m -> (E.z e. r c = (y i^i z) <-> E.z e. r c = (m i^i z)))
45	44	cbvrexv 2281	. . . . . . . . . . . . . . . . . 18 |- (E.y e. r E.z e. r c = (y i^i z) <-> E.m e. r E.z e. r c = (m i^i z))
46		ineq2 2790	. . . . . . . . . . . . . . . . . . . . 21 |- (z = n -> (m i^i z) = (m i^i n))
47	46	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . 20 |- (z = n -> (c = (m i^i z) <-> c = (m i^i n)))
48	47	cbvrexv 2281	. . . . . . . . . . . . . . . . . . 19 |- (E.z e. r c = (m i^i z) <-> E.n e. r c = (m i^i n))
49	48	rexbii 2128	. . . . . . . . . . . . . . . . . 18 |- (E.m e. r E.z e. r c = (m i^i z) <-> E.m e. r E.n e. r c = (m i^i n))
50	45, 49	bitri 190	. . . . . . . . . . . . . . . . 17 |- (E.y e. r E.z e. r c = (y i^i z) <-> E.m e. r E.n e. r c = (m i^i n))
51	50	abbii 2006	. . . . . . . . . . . . . . . 16 |- {c | E.y e. r E.z e. r c = (y i^i z)} = {c | E.m e. r E.n e. r c = (m i^i n)}
52	41, 51	eqtri 1908	. . . . . . . . . . . . . . 15 |- {w | E.y e. r E.z e. r w = (y i^i z)} = {c | E.m e. r E.n e. r c = (m i^i n)}
53	52	eqeq2i 1894	. . . . . . . . . . . . . 14 |- (s = {w | E.y e. r E.z e. r w = (y i^i z)} <-> s = {c | E.m e. r E.n e. r c = (m i^i n)})
54	53	opabbii 3402	. . . . . . . . . . . . 13 |- {<.r, s>. | s = {w | E.y e. r E.z e. r w = (y i^i z)}} = {<.r, s>. | s = {c | E.m e. r E.n e. r c = (m i^i n)}}
55	38, 54	eqtri 1908	. . . . . . . . . . . 12 |- {<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}} = {<.r, s>. | s = {c | E.m e. r E.n e. r c = (m i^i n)}}
56	55	fveq1i 4682	. . . . . . . . . . 11 |- ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) = ({<.r, s>. | s = {c | E.m e. r E.n e. r c = (m i^i n)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k))
57		fvex 4689	. . . . . . . . . . . 12 |- (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) e. _V
58	57	abrexex 4836	. . . . . . . . . . . . 13 |- {c | E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)} e. _V
59	57, 58	abrexex2 4847	. . . . . . . . . . . 12 |- {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)} e. _V
60		rexeq 2267	. . . . . . . . . . . . . 14 |- (r = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) -> (E.n e. r c = (m i^i n) <-> E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)))
61	60	rexeqbi1dv 2272	. . . . . . . . . . . . 13 |- (r = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) -> (E.m e. r E.n e. r c = (m i^i n) <-> E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)))
62	61	abbidv 2008	. . . . . . . . . . . 12 |- (r = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) -> {c | E.m e. r E.n e. r c = (m i^i n)} = {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)})
63	57, 59, 62	fvopab 4753	. . . . . . . . . . 11 |- ({<.r, s>. | s = {c | E.m e. r E.n e. r c = (m i^i n)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) = {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)}
64	56, 63	eqtri 1908	. . . . . . . . . 10 |- ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)) = {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)}
65	31, 64	syl6req 1945	. . . . . . . . 9 |- (((k e. om /\ n e. om) /\ n C_ k) -> {c | E.m e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)E.n e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k)c = (m i^i n)} = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k))
66	27, 65	sseqtrd 2653	. . . . . . . 8 |- (((k e. om /\ n e. om) /\ n C_ k) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k))
67		sstr 2625	. . . . . . . . 9 |- (((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) /\ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k)) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k))
68	67	expcom 403	. . . . . . . 8 |- ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k) -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k)))
69	66, 68	syl 12	. . . . . . 7 |- (((k e. om /\ n e. om) /\ n C_ k) -> ((rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` k) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc k)))
70	2, 4, 6, 8, 10, 69	findsg 3980	. . . . . 6 |- (((m e. om /\ n e. om) /\ n C_ m) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m))
71	70	adantll 428	. . . . 5 |- ((((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) /\ n C_ m) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) C_ (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m))
72	71	sseld 2619	. . . 4 |- ((((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) /\ n C_ m) -> (s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n) -> s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))
73	72	anim2d 620	. . 3 |- ((((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) /\ n C_ m) -> ((r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)) -> (r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m))))
74	73	ex 402	. 2 |- (((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) -> (n C_ m -> ((r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)) -> (r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))))
75		peano2 3972	. . . . . 6 |- (m e. om -> suc m e. om)
76	75	adantr 425	. . . . 5 |- ((m e. om /\ n e. om) -> suc m e. om)
77	76	ad2antlr 441	. . . 4 |- ((((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) /\ (n C_ m /\ (r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))) -> suc m e. om)
78		eqid 1884	. . . . . . . . 9 |- (r i^i s) = (r i^i s)
79		ineq1 2789	. . . . . . . . . . 11 |- (a = r -> (a i^i b) = (r i^i b))
80	79	eqeq2d 1895	. . . . . . . . . 10 |- (a = r -> ((r i^i s) = (a i^i b) <-> (r i^i s) = (r i^i b)))
81		ineq2 2790	. . . . . . . . . . 11 |- (b = s -> (r i^i b) = (r i^i s))
82	81	eqeq2d 1895	. . . . . . . . . 10 |- (b = s -> ((r i^i s) = (r i^i b) <-> (r i^i s) = (r i^i s)))
83	80, 82	rcla42ev 2385	. . . . . . . . 9 |- ((r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ (r i^i s) = (r i^i s)) -> E.a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)E.b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)(r i^i s) = (a i^i b))
84	78, 83	mp3an3 1180	. . . . . . . 8 |- ((r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)) -> E.a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)E.b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)(r i^i s) = (a i^i b))
85	84	ad2antll 443	. . . . . . 7 |- ((((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) /\ (n C_ m /\ (r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))) -> E.a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)E.b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)(r i^i s) = (a i^i b))
86		visset 2295	. . . . . . . . 9 |- r e. _V
87	86	inex1 3452	. . . . . . . 8 |- (r i^i s) e. _V
88		eqeq1 1890	. . . . . . . . 9 |- (c = (r i^i s) -> (c = (a i^i b) <-> (r i^i s) = (a i^i b)))
89	88	2rexbidv 2141	. . . . . . . 8 |- (c = (r i^i s) -> (E.a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)E.b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)c = (a i^i b) <-> E.a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)E.b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)(r i^i s) = (a i^i b)))
90	87, 89	elab 2403	. . . . . . 7 |- ((r i^i s) e. {c | E.a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)E.b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)c = (a i^i b)} <-> E.a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)E.b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)(r i^i s) = (a i^i b))
91	85, 90	sylibr 217	. . . . . 6 |- ((((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) /\ (n C_ m /\ (r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))) -> (r i^i s) e. {c | E.a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)E.b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)c = (a i^i b)})
92		fvex 4689	. . . . . . . 8 |- (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) e. _V
93	92	abrexex 4836	. . . . . . . . 9 |- {c | E.b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)c = (a i^i b)} e. _V
94	92, 93	abrexex2 4847	. . . . . . . 8 |- {c | E.a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)E.b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)c = (a i^i b)} e. _V
95		rexeq 2267	. . . . . . . . . 10 |- (k = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) -> (E.b e. k c = (a i^i b) <-> E.b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)c = (a i^i b)))
96	95	rexeqbi1dv 2272	. . . . . . . . 9 |- (k = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) -> (E.a e. k E.b e. k c = (a i^i b) <-> E.a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)E.b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)c = (a i^i b)))
97	96	abbidv 2008	. . . . . . . 8 |- (k = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) -> {c | E.a e. k E.b e. k c = (a i^i b)} = {c | E.a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)E.b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)c = (a i^i b)})
98	92, 94, 97	fvopab 4753	. . . . . . 7 |- ({<.k, t>. | t = {c | E.a e. k E.b e. k c = (a i^i b)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)) = {c | E.a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)E.b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)c = (a i^i b)}
99		ineq2 2790	. . . . . . . . . . . . . . . . 17 |- (b = z -> (a i^i b) = (a i^i z))
100	99	eqeq2d 1895	. . . . . . . . . . . . . . . 16 |- (b = z -> (c = (a i^i b) <-> c = (a i^i z)))
101	100	cbvrexv 2281	. . . . . . . . . . . . . . 15 |- (E.b e. k c = (a i^i b) <-> E.z e. k c = (a i^i z))
102	101	rexbii 2128	. . . . . . . . . . . . . 14 |- (E.a e. k E.b e. k c = (a i^i b) <-> E.a e. k E.z e. k c = (a i^i z))
103		ineq1 2789	. . . . . . . . . . . . . . . . 17 |- (a = y -> (a i^i z) = (y i^i z))
104	103	eqeq2d 1895	. . . . . . . . . . . . . . . 16 |- (a = y -> (c = (a i^i z) <-> c = (y i^i z)))
105	104	rexbidv 2124	. . . . . . . . . . . . . . 15 |- (a = y -> (E.z e. k c = (a i^i z) <-> E.z e. k c = (y i^i z)))
106	105	cbvrexv 2281	. . . . . . . . . . . . . 14 |- (E.a e. k E.z e. k c = (a i^i z) <-> E.y e. k E.z e. k c = (y i^i z))
107	102, 106	bitri 190	. . . . . . . . . . . . 13 |- (E.a e. k E.b e. k c = (a i^i b) <-> E.y e. k E.z e. k c = (y i^i z))
108	107	abbii 2006	. . . . . . . . . . . 12 |- {c | E.a e. k E.b e. k c = (a i^i b)} = {c | E.y e. k E.z e. k c = (y i^i z)}
109		eqeq1 1890	. . . . . . . . . . . . . 14 |- (c = w -> (c = (y i^i z) <-> w = (y i^i z)))
110	109	2rexbidv 2141	. . . . . . . . . . . . 13 |- (c = w -> (E.y e. k E.z e. k c = (y i^i z) <-> E.y e. k E.z e. k w = (y i^i z)))
111	110	cbvabv 2420	. . . . . . . . . . . 12 |- {c | E.y e. k E.z e. k c = (y i^i z)} = {w | E.y e. k E.z e. k w = (y i^i z)}
112	108, 111	eqtri 1908	. . . . . . . . . . 11 |- {c | E.a e. k E.b e. k c = (a i^i b)} = {w | E.y e. k E.z e. k w = (y i^i z)}
113	112	eqeq2i 1894	. . . . . . . . . 10 |- (t = {c | E.a e. k E.b e. k c = (a i^i b)} <-> t = {w | E.y e. k E.z e. k w = (y i^i z)})
114	113	opabbii 3402	. . . . . . . . 9 |- {<.k, t>. | t = {c | E.a e. k E.b e. k c = (a i^i b)}} = {<.k, t>. | t = {w | E.y e. k E.z e. k w = (y i^i z)}}
115		rexeq 2267	. . . . . . . . . . . . . 14 |- (k = u -> (E.z e. k w = (y i^i z) <-> E.z e. u w = (y i^i z)))
116	115	rexeqbi1dv 2272	. . . . . . . . . . . . 13 |- (k = u -> (E.y e. k E.z e. k w = (y i^i z) <-> E.y e. u E.z e. u w = (y i^i z)))
117	116	abbidv 2008	. . . . . . . . . . . 12 |- (k = u -> {w | E.y e. k E.z e. k w = (y i^i z)} = {w | E.y e. u E.z e. u w = (y i^i z)})
118	117	eqeq2d 1895	. . . . . . . . . . 11 |- (k = u -> (t = {w | E.y e. k E.z e. k w = (y i^i z)} <-> t = {w | E.y e. u E.z e. u w = (y i^i z)}))
119		eqeq1 1890	. . . . . . . . . . 11 |- (t = v -> (t = {w | E.y e. u E.z e. u w = (y i^i z)} <-> v = {w | E.y e. u E.z e. u w = (y i^i z)}))
120	118, 119	sylan9bb 599	. . . . . . . . . 10 |- ((k = u /\ t = v) -> (t = {w | E.y e. k E.z e. k w = (y i^i z)} <-> v = {w | E.y e. u E.z e. u w = (y i^i z)}))
121	120	cbvopabv 3404	. . . . . . . . 9 |- {<.k, t>. | t = {w | E.y e. k E.z e. k w = (y i^i z)}} = {<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}
122	114, 121	eqtri 1908	. . . . . . . 8 |- {<.k, t>. | t = {c | E.a e. k E.b e. k c = (a i^i b)}} = {<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}
123	122	fveq1i 4682	. . . . . . 7 |- ({<.k, t>. | t = {c | E.a e. k E.b e. k c = (a i^i b)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)) = ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m))
124	98, 123	eqtr3i 1910	. . . . . 6 |- {c | E.a e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)E.b e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)c = (a i^i b)} = ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m))
125	91, 124	syl6eleq 1981	. . . . 5 |- ((((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) /\ (n C_ m /\ (r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))) -> (r i^i s) e. ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))
126		nnon 3957	. . . . . . . 8 |- (m e. om -> m e. On)
127		rdgsuc 5153	. . . . . . . 8 |- (m e. On -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc m) = ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))
128	126, 127	syl 12	. . . . . . 7 |- (m e. om -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc m) = ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))
129	128	adantr 425	. . . . . 6 |- ((m e. om /\ n e. om) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc m) = ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))
130	129	ad2antlr 441	. . . . 5 |- ((((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) /\ (n C_ m /\ (r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))) -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc m) = ({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}` (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))
131	125, 130	eleqtrrd 1974	. . . 4 |- ((((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) /\ (n C_ m /\ (r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))) -> (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc m))
132		fveq2 4681	. . . . . 6 |- (x = suc m -> (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) = (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc m))
133	132	eleq2d 1964	. . . . 5 |- (x = suc m -> ((r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x) <-> (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc m)))
134	133	rcla4ev 2381	. . . 4 |- ((suc m e. om /\ (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` suc m)) -> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
135	77, 131, 134	syl11anc 524	. . 3 |- ((((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) /\ (n C_ m /\ (r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)))) -> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))
136	135	exp32 408	. 2 |- (((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) -> (n C_ m -> ((r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m)) -> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))))
137	74, 136	syldd 61	1 |- (((A e. B /\ A ~<_ om) /\ (m e. om /\ n e. om)) -> (n C_ m -> ((r e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` m) /\ s e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` n)) -> E.x e. om (r i^i s) e. (rec({<.u, v>. | v = {w | E.y e. u E.z e. u w = (y i^i z)}}, A)` x))))

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298   e. wcel 1300  {cab 1871  E.wrex 2106   i^i cin 2592   C_ wss 2593   class class class wbr 3338  {copab 3395  Oncon0 3657  suc csuc 3659  omcom 3949  ` cfv 3998  reccrdg 5139   ~<_ cdom 5424

This theorem is referenced by:  fictb 15371

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-rep 3428  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-3or 859  df-3an 860  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-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  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-fn 4009  df-fv 4014  df-rdg 5140

Copyright terms: Public domain