Theorem phi11lem1 4595

Description: Lemma for phi11 4596. (Contributed by SF, 3-Feb-2015.)

Assertion

Ref	Expression
phi11lem1	|- ( Phi A = Phi B -> A C_ B)

Proof of Theorem phi11lem1

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iftrue 3668	. . . . . . . . 9 |- (z e. Nn -> if(z e. Nn , (z +o 1c), z) = (z +o 1c))
2	1	eqcomd 2358	. . . . . . . 8 |- (z e. Nn -> (z +o 1c) = if(z e. Nn , (z +o 1c), z))
3		eleq1 2413	. . . . . . . . . . 11 |- (y = z -> (y e. Nn <-> z e. Nn ))
4		addceq1 4383	. . . . . . . . . . 11 |- (y = z -> (y +o 1c) = (z +o 1c))
5		id 19	. . . . . . . . . . 11 |- (y = z -> y = z)
6	3, 4, 5	ifbieq12d 3684	. . . . . . . . . 10 |- (y = z -> if(y e. Nn , (y +o 1c), y) = if(z e. Nn , (z +o 1c), z))
7	6	eqeq2d 2364	. . . . . . . . 9 |- (y = z -> ((z +o 1c) = if(y e. Nn , (y +o 1c), y) <-> (z +o 1c) = if(z e. Nn , (z +o 1c), z)))
8	7	rspcev 2955	. . . . . . . 8 |- ((z e. A /\ (z +o 1c) = if(z e. Nn , (z +o 1c), z)) -> E.y e. A (z +o 1c) = if(y e. Nn , (y +o 1c), y))
9	2, 8	sylan2 460	. . . . . . 7 |- ((z e. A /\ z e. Nn ) -> E.y e. A (z +o 1c) = if(y e. Nn , (y +o 1c), y))
10	9	ancoms 439	. . . . . 6 |- ((z e. Nn /\ z e. A) -> E.y e. A (z +o 1c) = if(y e. Nn , (y +o 1c), y))
11		vex 2862	. . . . . . . 8 |- z e. _V
12		1cex 4142	. . . . . . . 8 |- 1c e. _V
13	11, 12	addcex 4394	. . . . . . 7 |- (z +o 1c) e. _V
14		eqeq1 2359	. . . . . . . 8 |- (x = (z +o 1c) -> (x = if(y e. Nn , (y +o 1c), y) <-> (z +o 1c) = if(y e. Nn , (y +o 1c), y)))
15	14	rexbidv 2635	. . . . . . 7 |- (x = (z +o 1c) -> (E.y e. A x = if(y e. Nn , (y +o 1c), y) <-> E.y e. A (z +o 1c) = if(y e. Nn , (y +o 1c), y)))
16		df-phi 4565	. . . . . . 7 |- Phi A = {x | E.y e. A x = if(y e. Nn , (y +o 1c), y)}
17	13, 15, 16	elab2 2988	. . . . . 6 |- ((z +o 1c) e. Phi A <-> E.y e. A (z +o 1c) = if(y e. Nn , (y +o 1c), y))
18	10, 17	sylibr 203	. . . . 5 |- ((z e. Nn /\ z e. A) -> (z +o 1c) e. Phi A)
19		eleq2 2414	. . . . . . . . 9 |- ( Phi A = Phi B -> ((z +o 1c) e. Phi A <-> (z +o 1c) e. Phi B))
20	19	biimpac 472	. . . . . . . 8 |- (((z +o 1c) e. Phi A /\ Phi A = Phi B) -> (z +o 1c) e. Phi B)
21	14	rexbidv 2635	. . . . . . . . . 10 |- (x = (z +o 1c) -> (E.y e. B x = if(y e. Nn , (y +o 1c), y) <-> E.y e. B (z +o 1c) = if(y e. Nn , (y +o 1c), y)))
22		df-phi 4565	. . . . . . . . . 10 |- Phi B = {x | E.y e. B x = if(y e. Nn , (y +o 1c), y)}
23	13, 21, 22	elab2 2988	. . . . . . . . 9 |- ((z +o 1c) e. Phi B <-> E.y e. B (z +o 1c) = if(y e. Nn , (y +o 1c), y))
24		iffalse 3669	. . . . . . . . . . . . . . . . . . 19 |- (-. y e. Nn -> if(y e. Nn , (y +o 1c), y) = y)
25	24	eqeq2d 2364	. . . . . . . . . . . . . . . . . 18 |- (-. y e. Nn -> ((z +o 1c) = if(y e. Nn , (y +o 1c), y) <-> (z +o 1c) = y))
26	25	biimpac 472	. . . . . . . . . . . . . . . . 17 |- (((z +o 1c) = if(y e. Nn , (y +o 1c), y) /\ -. y e. Nn ) -> (z +o 1c) = y)
27		peano2 4403	. . . . . . . . . . . . . . . . . 18 |- (z e. Nn -> (z +o 1c) e. Nn )
28		eleq1 2413	. . . . . . . . . . . . . . . . . 18 |- ((z +o 1c) = y -> ((z +o 1c) e. Nn <-> y e. Nn ))
29	27, 28	syl5ibcom 211	. . . . . . . . . . . . . . . . 17 |- (z e. Nn -> ((z +o 1c) = y -> y e. Nn ))
30	26, 29	syl5 28	. . . . . . . . . . . . . . . 16 |- (z e. Nn -> (((z +o 1c) = if(y e. Nn , (y +o 1c), y) /\ -. y e. Nn ) -> y e. Nn ))
31	30	expdimp 426	. . . . . . . . . . . . . . 15 |- ((z e. Nn /\ (z +o 1c) = if(y e. Nn , (y +o 1c), y)) -> (-. y e. Nn -> y e. Nn ))
32	31	pm2.18d 103	. . . . . . . . . . . . . 14 |- ((z e. Nn /\ (z +o 1c) = if(y e. Nn , (y +o 1c), y)) -> y e. Nn )
33		simpl 443	. . . . . . . . . . . . . 14 |- ((z e. Nn /\ (z +o 1c) = if(y e. Nn , (y +o 1c), y)) -> z e. Nn )
34		simpr 447	. . . . . . . . . . . . . . 15 |- ((z e. Nn /\ (z +o 1c) = if(y e. Nn , (y +o 1c), y)) -> (z +o 1c) = if(y e. Nn , (y +o 1c), y))
35		iftrue 3668	. . . . . . . . . . . . . . . 16 |- (y e. Nn -> if(y e. Nn , (y +o 1c), y) = (y +o 1c))
36	32, 35	syl 15	. . . . . . . . . . . . . . 15 |- ((z e. Nn /\ (z +o 1c) = if(y e. Nn , (y +o 1c), y)) -> if(y e. Nn , (y +o 1c), y) = (y +o 1c))
37	34, 36	eqtr2d 2386	. . . . . . . . . . . . . 14 |- ((z e. Nn /\ (z +o 1c) = if(y e. Nn , (y +o 1c), y)) -> (y +o 1c) = (z +o 1c))
38		peano4 4557	. . . . . . . . . . . . . 14 |- ((y e. Nn /\ z e. Nn /\ (y +o 1c) = (z +o 1c)) -> y = z)
39	32, 33, 37, 38	syl3anc 1182	. . . . . . . . . . . . 13 |- ((z e. Nn /\ (z +o 1c) = if(y e. Nn , (y +o 1c), y)) -> y = z)
40	39	3adant2 974	. . . . . . . . . . . 12 |- ((z e. Nn /\ y e. B /\ (z +o 1c) = if(y e. Nn , (y +o 1c), y)) -> y = z)
41		simp2 956	. . . . . . . . . . . 12 |- ((z e. Nn /\ y e. B /\ (z +o 1c) = if(y e. Nn , (y +o 1c), y)) -> y e. B)
42	40, 41	eqeltrrd 2428	. . . . . . . . . . 11 |- ((z e. Nn /\ y e. B /\ (z +o 1c) = if(y e. Nn , (y +o 1c), y)) -> z e. B)
43	42	3expia 1153	. . . . . . . . . 10 |- ((z e. Nn /\ y e. B) -> ((z +o 1c) = if(y e. Nn , (y +o 1c), y) -> z e. B))
44	43	rexlimdva 2738	. . . . . . . . 9 |- (z e. Nn -> (E.y e. B (z +o 1c) = if(y e. Nn , (y +o 1c), y) -> z e. B))
45	23, 44	syl5bi 208	. . . . . . . 8 |- (z e. Nn -> ((z +o 1c) e. Phi B -> z e. B))
46	20, 45	syl5 28	. . . . . . 7 |- (z e. Nn -> (((z +o 1c) e. Phi A /\ Phi A = Phi B) -> z e. B))
47	46	exp3a 425	. . . . . 6 |- (z e. Nn -> ((z +o 1c) e. Phi A -> ( Phi A = Phi B -> z e. B)))
48	47	adantr 451	. . . . 5 |- ((z e. Nn /\ z e. A) -> ((z +o 1c) e. Phi A -> ( Phi A = Phi B -> z e. B)))
49	18, 48	mpd 14	. . . 4 |- ((z e. Nn /\ z e. A) -> ( Phi A = Phi B -> z e. B))
50		iffalse 3669	. . . . . . . . 9 |- (-. z e. Nn -> if(z e. Nn , (z +o 1c), z) = z)
51	50	eqcomd 2358	. . . . . . . 8 |- (-. z e. Nn -> z = if(z e. Nn , (z +o 1c), z))
52	6	eqeq2d 2364	. . . . . . . . 9 |- (y = z -> (z = if(y e. Nn , (y +o 1c), y) <-> z = if(z e. Nn , (z +o 1c), z)))
53	52	rspcev 2955	. . . . . . . 8 |- ((z e. A /\ z = if(z e. Nn , (z +o 1c), z)) -> E.y e. A z = if(y e. Nn , (y +o 1c), y))
54	51, 53	sylan2 460	. . . . . . 7 |- ((z e. A /\ -. z e. Nn ) -> E.y e. A z = if(y e. Nn , (y +o 1c), y))
55	54	ancoms 439	. . . . . 6 |- ((-. z e. Nn /\ z e. A) -> E.y e. A z = if(y e. Nn , (y +o 1c), y))
56		eqeq1 2359	. . . . . . . 8 |- (x = z -> (x = if(y e. Nn , (y +o 1c), y) <-> z = if(y e. Nn , (y +o 1c), y)))
57	56	rexbidv 2635	. . . . . . 7 |- (x = z -> (E.y e. A x = if(y e. Nn , (y +o 1c), y) <-> E.y e. A z = if(y e. Nn , (y +o 1c), y)))
58	11, 57, 16	elab2 2988	. . . . . 6 |- (z e. Phi A <-> E.y e. A z = if(y e. Nn , (y +o 1c), y))
59	55, 58	sylibr 203	. . . . 5 |- ((-. z e. Nn /\ z e. A) -> z e. Phi A)
60		eleq2 2414	. . . . . . . . 9 |- ( Phi A = Phi B -> (z e. Phi A <-> z e. Phi B))
61	60	biimpac 472	. . . . . . . 8 |- ((z e. Phi A /\ Phi A = Phi B) -> z e. Phi B)
62	56	rexbidv 2635	. . . . . . . . . 10 |- (x = z -> (E.y e. B x = if(y e. Nn , (y +o 1c), y) <-> E.y e. B z = if(y e. Nn , (y +o 1c), y)))
63	11, 62, 22	elab2 2988	. . . . . . . . 9 |- (z e. Phi B <-> E.y e. B z = if(y e. Nn , (y +o 1c), y))
64		simpr 447	. . . . . . . . . . . . . 14 |- ((-. z e. Nn /\ z = if(y e. Nn , (y +o 1c), y)) -> z = if(y e. Nn , (y +o 1c), y))
65	35	eqeq2d 2364	. . . . . . . . . . . . . . . . . . 19 |- (y e. Nn -> (z = if(y e. Nn , (y +o 1c), y) <-> z = (y +o 1c)))
66		peano2 4403	. . . . . . . . . . . . . . . . . . . 20 |- (y e. Nn -> (y +o 1c) e. Nn )
67		eleq1a 2422	. . . . . . . . . . . . . . . . . . . 20 |- ((y +o 1c) e. Nn -> (z = (y +o 1c) -> z e. Nn ))
68	66, 67	syl 15	. . . . . . . . . . . . . . . . . . 19 |- (y e. Nn -> (z = (y +o 1c) -> z e. Nn ))
69	65, 68	sylbid 206	. . . . . . . . . . . . . . . . . 18 |- (y e. Nn -> (z = if(y e. Nn , (y +o 1c), y) -> z e. Nn ))
70	69	com12 27	. . . . . . . . . . . . . . . . 17 |- (z = if(y e. Nn , (y +o 1c), y) -> (y e. Nn -> z e. Nn ))
71	70	con3d 125	. . . . . . . . . . . . . . . 16 |- (z = if(y e. Nn , (y +o 1c), y) -> (-. z e. Nn -> -. y e. Nn ))
72	71	impcom 419	. . . . . . . . . . . . . . 15 |- ((-. z e. Nn /\ z = if(y e. Nn , (y +o 1c), y)) -> -. y e. Nn )
73	72, 24	syl 15	. . . . . . . . . . . . . 14 |- ((-. z e. Nn /\ z = if(y e. Nn , (y +o 1c), y)) -> if(y e. Nn , (y +o 1c), y) = y)
74	64, 73	eqtr2d 2386	. . . . . . . . . . . . 13 |- ((-. z e. Nn /\ z = if(y e. Nn , (y +o 1c), y)) -> y = z)
75	74	adantlr 695	. . . . . . . . . . . 12 |- (((-. z e. Nn /\ y e. B) /\ z = if(y e. Nn , (y +o 1c), y)) -> y = z)
76		simplr 731	. . . . . . . . . . . 12 |- (((-. z e. Nn /\ y e. B) /\ z = if(y e. Nn , (y +o 1c), y)) -> y e. B)
77	75, 76	eqeltrrd 2428	. . . . . . . . . . 11 |- (((-. z e. Nn /\ y e. B) /\ z = if(y e. Nn , (y +o 1c), y)) -> z e. B)
78	77	ex 423	. . . . . . . . . 10 |- ((-. z e. Nn /\ y e. B) -> (z = if(y e. Nn , (y +o 1c), y) -> z e. B))
79	78	rexlimdva 2738	. . . . . . . . 9 |- (-. z e. Nn -> (E.y e. B z = if(y e. Nn , (y +o 1c), y) -> z e. B))
80	63, 79	syl5bi 208	. . . . . . . 8 |- (-. z e. Nn -> (z e. Phi B -> z e. B))
81	61, 80	syl5 28	. . . . . . 7 |- (-. z e. Nn -> ((z e. Phi A /\ Phi A = Phi B) -> z e. B))
82	81	exp3a 425	. . . . . 6 |- (-. z e. Nn -> (z e. Phi A -> ( Phi A = Phi B -> z e. B)))
83	82	adantr 451	. . . . 5 |- ((-. z e. Nn /\ z e. A) -> (z e. Phi A -> ( Phi A = Phi B -> z e. B)))
84	59, 83	mpd 14	. . . 4 |- ((-. z e. Nn /\ z e. A) -> ( Phi A = Phi B -> z e. B))
85	49, 84	pm2.61ian 765	. . 3 |- (z e. A -> ( Phi A = Phi B -> z e. B))
86	85	com12 27	. 2 |- ( Phi A = Phi B -> (z e. A -> z e. B))
87	86	ssrdv 3278	1 |- ( Phi A = Phi B -> A C_ B)

Syntax hints:  -. wn 3   -> wi 4   /\ wa 358   /\ w3a 934   = wceq 1642   e. wcel 1710  E.wrex 2615   C_ wss 3257  ifcif 3662  1_cc1c 4134   Nn cnnc 4373   +o cplc 4375   Phi cphi 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565

This theorem is referenced by:  phi11  4596