Theorem axfelem12 14957

Description: Lemma for axfe (future) . The surreal mentioned in the previous lemma will ultimately be the union of C. Again, we just change bound variables for later.

Hypothesis

Ref	Expression
axfelem12.1	|- C = {f | E.g e. L E.h e. R E.a e. P ((g |` a) = f /\ (h |` a) = f)}

Assertion

Ref	Expression
axfelem12	|- C = {b | E.c e. L E.d e. R E.e e. P ((c |` e) = b /\ (d |` e) = b)}

Distinct variable groups:   a,b,c,d,e,f   g,h,a,b,c   h,d   f,g,h   L,b,c,f,g   P,a,b,c,d,e,f   P,g,h   R,b,c,d,f   R,g,h

Proof of Theorem axfelem12

Step	Hyp	Ref	Expression
1		axfelem12.1	. 2 |- C = {f | E.g e. L E.h e. R E.a e. P ((g |` a) = f /\ (h |` a) = f)}
2		eqeq2 2179	. . . . . . 7 |- (f = b -> ((g |` a) = f <-> (g |` a) = b))
3		eqeq2 2179	. . . . . . 7 |- (f = b -> ((h |` a) = f <-> (h |` a) = b))
4	2, 3	anbi12d 821	. . . . . 6 |- (f = b -> (((g |` a) = f /\ (h |` a) = f) <-> ((g |` a) = b /\ (h |` a) = b)))
5	4	rexbidv 2404	. . . . 5 |- (f = b -> (E.a e. P ((g |` a) = f /\ (h |` a) = f) <-> E.a e. P ((g |` a) = b /\ (h |` a) = b)))
6	5	2rexbidv 2421	. . . 4 |- (f = b -> (E.g e. L E.h e. R E.a e. P ((g |` a) = f /\ (h |` a) = f) <-> E.g e. L E.h e. R E.a e. P ((g |` a) = b /\ (h |` a) = b)))
7		reseq1 4370	. . . . . . . . 9 |- (g = c -> (g |` a) = (c |` a))
8	7	eqeq1d 2178	. . . . . . . 8 |- (g = c -> ((g |` a) = b <-> (c |` a) = b))
9	8	anbi1d 815	. . . . . . 7 |- (g = c -> (((g |` a) = b /\ (h |` a) = b) <-> ((c |` a) = b /\ (h |` a) = b)))
10	9	2rexbidv 2421	. . . . . 6 |- (g = c -> (E.h e. R E.a e. P ((g |` a) = b /\ (h |` a) = b) <-> E.h e. R E.a e. P ((c |` a) = b /\ (h |` a) = b)))
11	10	cbvrexv 2558	. . . . 5 |- (E.g e. L E.h e. R E.a e. P ((g |` a) = b /\ (h |` a) = b) <-> E.c e. L E.h e. R E.a e. P ((c |` a) = b /\ (h |` a) = b))
12		reseq1 4370	. . . . . . . . . . 11 |- (h = d -> (h |` a) = (d |` a))
13	12	eqeq1d 2178	. . . . . . . . . 10 |- (h = d -> ((h |` a) = b <-> (d |` a) = b))
14	13	anbi2d 814	. . . . . . . . 9 |- (h = d -> (((c |` a) = b /\ (h |` a) = b) <-> ((c |` a) = b /\ (d |` a) = b)))
15	14	rexbidv 2404	. . . . . . . 8 |- (h = d -> (E.a e. P ((c |` a) = b /\ (h |` a) = b) <-> E.a e. P ((c |` a) = b /\ (d |` a) = b)))
16	15	cbvrexv 2558	. . . . . . 7 |- (E.h e. R E.a e. P ((c |` a) = b /\ (h |` a) = b) <-> E.d e. R E.a e. P ((c |` a) = b /\ (d |` a) = b))
17		reseq2 4371	. . . . . . . . . . 11 |- (a = e -> (c |` a) = (c |` e))
18	17	eqeq1d 2178	. . . . . . . . . 10 |- (a = e -> ((c |` a) = b <-> (c |` e) = b))
19		reseq2 4371	. . . . . . . . . . 11 |- (a = e -> (d |` a) = (d |` e))
20	19	eqeq1d 2178	. . . . . . . . . 10 |- (a = e -> ((d |` a) = b <-> (d |` e) = b))
21	18, 20	anbi12d 821	. . . . . . . . 9 |- (a = e -> (((c |` a) = b /\ (d |` a) = b) <-> ((c |` e) = b /\ (d |` e) = b)))
22	21	cbvrexv 2558	. . . . . . . 8 |- (E.a e. P ((c |` a) = b /\ (d |` a) = b) <-> E.e e. P ((c |` e) = b /\ (d |` e) = b))
23	22	rexbii 2408	. . . . . . 7 |- (E.d e. R E.a e. P ((c |` a) = b /\ (d |` a) = b) <-> E.d e. R E.e e. P ((c |` e) = b /\ (d |` e) = b))
24	16, 23	bitri 306	. . . . . 6 |- (E.h e. R E.a e. P ((c |` a) = b /\ (h |` a) = b) <-> E.d e. R E.e e. P ((c |` e) = b /\ (d |` e) = b))
25	24	rexbii 2408	. . . . 5 |- (E.c e. L E.h e. R E.a e. P ((c |` a) = b /\ (h |` a) = b) <-> E.c e. L E.d e. R E.e e. P ((c |` e) = b /\ (d |` e) = b))
26	11, 25	bitri 306	. . . 4 |- (E.g e. L E.h e. R E.a e. P ((g |` a) = b /\ (h |` a) = b) <-> E.c e. L E.d e. R E.e e. P ((c |` e) = b /\ (d |` e) = b))
27	6, 26	syl6bb 324	. . 3 |- (f = b -> (E.g e. L E.h e. R E.a e. P ((g |` a) = f /\ (h |` a) = f) <-> E.c e. L E.d e. R E.e e. P ((c |` e) = b /\ (d |` e) = b)))
28	27	cbvabv 2692	. 2 |- {f | E.g e. L E.h e. R E.a e. P ((g |` a) = f /\ (h |` a) = f)} = {b | E.c e. L E.d e. R E.e e. P ((c |` e) = b /\ (d |` e) = b)}
29	1, 28	eqtri 2190	1 |- C = {b | E.c e. L E.d e. R E.e e. P ((c |` e) = b /\ (d |` e) = b)}

Syntax hints:   /\ wa 433   = wceq 1615  {cab 2157  E.wrex 2386   |` cres 4153

This theorem is referenced by:  axfelem18 14963  axfelem19 14964  axfelem20 14965  axfelem22 14967

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-ex 1645  df-sb 1845  df-clab 2158  df-cleq 2163  df-clel 2166  df-rex 2390  df-v 2571  df-in 2866  df-opab 3598  df-xp 4165  df-res 4171

Copyright terms: Public domain