Theorem canthnumlem 9056

Description: Lemma for canthnum 9057. (Contributed by Mario Carneiro, 19-May-2015.)

Hypotheses

Ref	Expression
canth4.1	|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) }
canth4.2	|- B = U. dom W
canth4.3	|- C = ( `' ( W ` B ) " { ( F ` B ) } )

Assertion

Ref	Expression
canthnumlem	|- ( A e. V -> -. F : ( ~P A i^i dom card ) -1-1-> A )

Distinct variable groups:   x, r, y, A   B, r, x, y   F, r, x, y   V, r, x, y   y, C   W, r, x, y

Allowed substitution hints:   C( x, r)

Proof of Theorem canthnumlem

Step	Hyp	Ref	Expression
1		f1f 5764	. . . . 5 |- ( F : ( ~P A i^i dom card ) -1-1-> A -> F : ( ~P A i^i dom card ) --> A )
2		ssid 3461	. . . . . 6 |- ( ~P A i^i dom card ) C_ ( ~P A i^i dom card )
3		canth4.1	. . . . . . 7 |- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) }
4		canth4.2	. . . . . . 7 |- B = U. dom W
5		canth4.3	. . . . . . 7 |- C = ( `' ( W ` B ) " { ( F ` B ) } )
6	3, 4, 5	canth4 9055	. . . . . 6 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) --> A /\ ( ~P A i^i dom card ) C_ ( ~P A i^i dom card ) ) -> ( B C_ A /\ C C. B /\ ( F ` B ) = ( F ` C ) ) )
7	2, 6	mp3an3 1315	. . . . 5 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) --> A ) -> ( B C_ A /\ C C. B /\ ( F ` B ) = ( F ` C ) ) )
8	1, 7	sylan2 472	. . . 4 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( B C_ A /\ C C. B /\ ( F ` B ) = ( F ` C ) ) )
9	8	simp3d 1011	. . 3 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( F ` B ) = ( F ` C ) )
10		simpr 459	. . . 4 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> F : ( ~P A i^i dom card ) -1-1-> A )
11	8	simp1d 1009	. . . . . 6 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> B C_ A )
12		elpw2g 4557	. . . . . . 7 |- ( A e. V -> ( B e. ~P A <-> B C_ A ) )
13	12	adantr 463	. . . . . 6 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( B e. ~P A <-> B C_ A ) )
14	11, 13	mpbird 232	. . . . 5 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> B e. ~P A )
15		eqid 2402	. . . . . . . . . . . . 13 |- B = B
16		eqid 2402	. . . . . . . . . . . . 13 |- ( W ` B ) = ( W ` B )
17	15, 16	pm3.2i 453	. . . . . . . . . . . 12 |- ( B = B /\ ( W ` B ) = ( W ` B ) )
18		elex 3068	. . . . . . . . . . . . . 14 |- ( A e. V -> A e. _V )
19	18	adantr 463	. . . . . . . . . . . . 13 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> A e. _V )
20	10, 1	syl 17	. . . . . . . . . . . . . 14 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> F : ( ~P A i^i dom card ) --> A )
21	20	ffvelrnda 6009	. . . . . . . . . . . . 13 |- ( ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) /\ x e. ( ~P A i^i dom card ) ) -> ( F ` x ) e. A )
22	3, 19, 21, 4	fpwwe 9054	. . . . . . . . . . . 12 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( ( B W ( W ` B ) /\ ( F ` B ) e. B ) <-> ( B = B /\ ( W ` B ) = ( W ` B ) ) ) )
23	17, 22	mpbiri 233	. . . . . . . . . . 11 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( B W ( W ` B ) /\ ( F ` B ) e. B ) )
24	23	simpld 457	. . . . . . . . . 10 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> B W ( W ` B ) )
25	3, 19	fpwwelem 9053	. . . . . . . . . 10 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( B W ( W ` B ) <-> ( ( B C_ A /\ ( W ` B ) C_ ( B X. B ) ) /\ ( ( W ` B ) We B /\ A. y e. B ( F ` ( `' ( W ` B ) " { y } ) ) = y ) ) ) )
26	24, 25	mpbid 210	. . . . . . . . 9 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( ( B C_ A /\ ( W ` B ) C_ ( B X. B ) ) /\ ( ( W ` B ) We B /\ A. y e. B ( F ` ( `' ( W ` B ) " { y } ) ) = y ) ) )
27	26	simprd 461	. . . . . . . 8 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( ( W ` B ) We B /\ A. y e. B ( F ` ( `' ( W ` B ) " { y } ) ) = y ) )
28	27	simpld 457	. . . . . . 7 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( W ` B ) We B )
29		fvex 5859	. . . . . . . 8 |- ( W ` B ) e. _V
30		weeq1 4811	. . . . . . . 8 |- ( r = ( W ` B ) -> ( r We B <-> ( W ` B ) We B ) )
31	29, 30	spcev 3151	. . . . . . 7 |- ( ( W ` B ) We B -> E. r r We B )
32	28, 31	syl 17	. . . . . 6 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> E. r r We B )
33		ween 8448	. . . . . 6 |- ( B e. dom card <-> E. r r We B )
34	32, 33	sylibr 212	. . . . 5 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> B e. dom card )
35	14, 34	elind 3627	. . . 4 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> B e. ( ~P A i^i dom card ) )
36	8	simp2d 1010	. . . . . . . 8 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> C C. B )
37	36	pssssd 3540	. . . . . . 7 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> C C_ B )
38	37, 11	sstrd 3452	. . . . . 6 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> C C_ A )
39		elpw2g 4557	. . . . . . 7 |- ( A e. V -> ( C e. ~P A <-> C C_ A ) )
40	39	adantr 463	. . . . . 6 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( C e. ~P A <-> C C_ A ) )
41	38, 40	mpbird 232	. . . . 5 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> C e. ~P A )
42		ssnum 8452	. . . . . 6 |- ( ( B e. dom card /\ C C_ B ) -> C e. dom card )
43	34, 37, 42	syl2anc 659	. . . . 5 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> C e. dom card )
44	41, 43	elind 3627	. . . 4 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> C e. ( ~P A i^i dom card ) )
45		f1fveq 6151	. . . 4 |- ( ( F : ( ~P A i^i dom card ) -1-1-> A /\ ( B e. ( ~P A i^i dom card ) /\ C e. ( ~P A i^i dom card ) ) ) -> ( ( F ` B ) = ( F ` C ) <-> B = C ) )
46	10, 35, 44, 45	syl12anc 1228	. . 3 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( ( F ` B ) = ( F ` C ) <-> B = C ) )
47	9, 46	mpbid 210	. 2 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> B = C )
48	36	pssned 3541	. . . 4 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> C =/= B )
49	48	necomd 2674	. . 3 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> B =/= C )
50	49	neneqd 2605	. 2 |- ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> -. B = C )
51	47, 50	pm2.65da 574	1 |- ( A e. V -> -. F : ( ~P A i^i dom card ) -1-1-> A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 367   /\ w3a 974   = wceq 1405   E.wex 1633   e. wcel 1842   A.wral 2754   _Vcvv 3059   i^i cin 3413   C_ wss 3414   C. wpss 3415   ~Pcpw 3955   {csn 3972   U.cuni 4191   class class class wbr 4395   {copab 4452   We wwe 4781   X. cxp 4821   `'ccnv 4822   dom cdm 4823   "cima 4826   -->wf 5565   -1-1->wf1 5566   ` cfv 5569   cardccrd 8348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-reu 2761  df-rmo 2762  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-int 4228  df-iun 4273  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-se 4783  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-pred 5367  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-isom 5578  df-riota 6240  df-ov 6281  df-1st 6784  df-wrecs 7013  df-recs 7075  df-er 7348  df-en 7555  df-dom 7556  df-oi 7969  df-card 8352

This theorem is referenced by:  canthnum  9057