Theorem ptcmplem4 21054

Description: Lemma for ptcmp 21057. (Contributed by Mario Carneiro, 26-Aug-2015.)

Hypotheses

Ref	Expression
ptcmp.1	|- S = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )
ptcmp.2	|- X = X_ n e. A U. ( F ` n )
ptcmp.3	|- ( ph -> A e. V )
ptcmp.4	|- ( ph -> F : A --> Comp )
ptcmp.5	|- ( ph -> X e. (UFL i^i dom card ) )
ptcmplem2.5	|- ( ph -> U C_ ran S )
ptcmplem2.6	|- ( ph -> X = U. U )
ptcmplem2.7	|- ( ph -> -. E. z e. ( ~P U i^i Fin ) X = U. z )
ptcmplem3.8	|- K = { u e. ( F ` k ) | ( `' ( w e. X |-> ( w ` k ) ) " u ) e. U }

Assertion

Ref	Expression
ptcmplem4	|- -. ph

Distinct variable groups:   k, n, u, w, z, A   u, K   S, k, n, u, z   ph, k, n, u   U, k, u, z   k, V, n, u, w, z   k, F, n, u, w, z   k, X, n, u, w, z

Allowed substitution hints:   ph( z, w)   S( w)   U( w, n)   K( z, w, k, n)

Proof of Theorem ptcmplem4

Dummy variables f v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ptcmp.1	. . 3 |- S = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )
2		ptcmp.2	. . 3 |- X = X_ n e. A U. ( F ` n )
3		ptcmp.3	. . 3 |- ( ph -> A e. V )
4		ptcmp.4	. . 3 |- ( ph -> F : A --> Comp )
5		ptcmp.5	. . 3 |- ( ph -> X e. (UFL i^i dom card ) )
6		ptcmplem2.5	. . 3 |- ( ph -> U C_ ran S )
7		ptcmplem2.6	. . 3 |- ( ph -> X = U. U )
8		ptcmplem2.7	. . 3 |- ( ph -> -. E. z e. ( ~P U i^i Fin ) X = U. z )
9		ptcmplem3.8	. . 3 |- K = { u e. ( F ` k ) | ( `' ( w e. X |-> ( w ` k ) ) " u ) e. U }
10	1, 2, 3, 4, 5, 6, 7, 8, 9	ptcmplem3 21053	. 2 |- ( ph -> E. f ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) )
11		simprl 762	. . . . . . . . 9 |- ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> f Fn A )
12		eldifi 3587	. . . . . . . . . . . 12 |- ( ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> ( f ` k ) e. U. ( F ` k ) )
13	12	ralimi 2818	. . . . . . . . . . 11 |- ( A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> A. k e. A ( f ` k ) e. U. ( F ` k ) )
14		fveq2 5877	. . . . . . . . . . . . 13 |- ( n = k -> ( f ` n ) = ( f ` k ) )
15		fveq2 5877	. . . . . . . . . . . . . 14 |- ( n = k -> ( F ` n ) = ( F ` k ) )
16	15	unieqd 4226	. . . . . . . . . . . . 13 |- ( n = k -> U. ( F ` n ) = U. ( F ` k ) )
17	14, 16	eleq12d 2504	. . . . . . . . . . . 12 |- ( n = k -> ( ( f ` n ) e. U. ( F ` n ) <-> ( f ` k ) e. U. ( F ` k ) ) )
18	17	cbvralv 3055	. . . . . . . . . . 11 |- ( A. n e. A ( f ` n ) e. U. ( F ` n ) <-> A. k e. A ( f ` k ) e. U. ( F ` k ) )
19	13, 18	sylibr 215	. . . . . . . . . 10 |- ( A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> A. n e. A ( f ` n ) e. U. ( F ` n ) )
20	19	ad2antll 733	. . . . . . . . 9 |- ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> A. n e. A ( f ` n ) e. U. ( F ` n ) )
21		vex 3084	. . . . . . . . . 10 |- f e. _V
22	21	elixp 7533	. . . . . . . . 9 |- ( f e. X_ n e. A U. ( F ` n ) <-> ( f Fn A /\ A. n e. A ( f ` n ) e. U. ( F ` n ) ) )
23	11, 20, 22	sylanbrc 668	. . . . . . . 8 |- ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> f e. X_ n e. A U. ( F ` n ) )
24	23, 2	syl6eleqr 2521	. . . . . . 7 |- ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> f e. X )
25	7	adantr 466	. . . . . . 7 |- ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> X = U. U )
26	24, 25	eleqtrd 2512	. . . . . 6 |- ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> f e. U. U )
27		eluni2 4220	. . . . . 6 |- ( f e. U. U <-> E. v e. U f e. v )
28	26, 27	sylib 199	. . . . 5 |- ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> E. v e. U f e. v )
29		simplrr 769	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> f e. v )
30	29	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> f e. v )
31		simprr 764	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> v = ( `' ( w e. X |-> ( w ` k ) ) " u ) )
32	30, 31	eleqtrd 2512	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> f e. ( `' ( w e. X |-> ( w ` k ) ) " u ) )
33		fveq1 5876	. . . . . . . . . . . . . . . . . 18 |- ( w = f -> ( w ` k ) = ( f ` k ) )
34	33	eleq1d 2491	. . . . . . . . . . . . . . . . 17 |- ( w = f -> ( ( w ` k ) e. u <-> ( f ` k ) e. u ) )
35		eqid 2422	. . . . . . . . . . . . . . . . . 18 |- ( w e. X |-> ( w ` k ) ) = ( w e. X |-> ( w ` k ) )
36	35	mptpreima 5343	. . . . . . . . . . . . . . . . 17 |- ( `' ( w e. X |-> ( w ` k ) ) " u ) = { w e. X | ( w ` k ) e. u }
37	34, 36	elrab2 3231	. . . . . . . . . . . . . . . 16 |- ( f e. ( `' ( w e. X |-> ( w ` k ) ) " u ) <-> ( f e. X /\ ( f ` k ) e. u ) )
38	37	simprbi 465	. . . . . . . . . . . . . . 15 |- ( f e. ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. u )
39	32, 38	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> ( f ` k ) e. u )
40		simprl 762	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> u e. ( F ` k ) )
41		simplrl 768	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> v e. U )
42	41	adantr 466	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> v e. U )
43	31, 42	eqeltrrd 2511	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> ( `' ( w e. X |-> ( w ` k ) ) " u ) e. U )
44		rabid 3005	. . . . . . . . . . . . . . . 16 |- ( u e. { u e. ( F ` k ) | ( `' ( w e. X |-> ( w ` k ) ) " u ) e. U } <-> ( u e. ( F ` k ) /\ ( `' ( w e. X |-> ( w ` k ) ) " u ) e. U ) )
45	40, 43, 44	sylanbrc 668	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> u e. { u e. ( F ` k ) | ( `' ( w e. X |-> ( w ` k ) ) " u ) e. U } )
46	45, 9	syl6eleqr 2521	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> u e. K )
47		elunii 4221	. . . . . . . . . . . . . 14 |- ( ( ( f ` k ) e. u /\ u e. K ) -> ( f ` k ) e. U. K )
48	39, 46, 47	syl2anc 665	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> ( f ` k ) e. U. K )
49	48	rexlimdvaa 2918	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) )
50	49	expr 618	. . . . . . . . . . 11 |- ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ k e. A ) -> ( ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) ) )
51	50	ralimdva 2833	. . . . . . . . . 10 |- ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) -> ( A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> A. k e. A ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) ) )
52	51	ex 435	. . . . . . . . 9 |- ( ( ph /\ f Fn A ) -> ( ( v e. U /\ f e. v ) -> ( A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> A. k e. A ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) ) ) )
53	52	com23 81	. . . . . . . 8 |- ( ( ph /\ f Fn A ) -> ( A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> ( ( v e. U /\ f e. v ) -> A. k e. A ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) ) ) )
54	53	impr 623	. . . . . . 7 |- ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> ( ( v e. U /\ f e. v ) -> A. k e. A ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) ) )
55	54	imp 430	. . . . . 6 |- ( ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( v e. U /\ f e. v ) ) -> A. k e. A ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) )
56	6	adantr 466	. . . . . . . . . 10 |- ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> U C_ ran S )
57	56	sselda 3464	. . . . . . . . 9 |- ( ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ v e. U ) -> v e. ran S )
58	57	adantrr 721	. . . . . . . 8 |- ( ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( v e. U /\ f e. v ) ) -> v e. ran S )
59	1	rnmpt2 6416	. . . . . . . 8 |- ran S = { v | E. k e. A E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) }
60	58, 59	syl6eleq 2520	. . . . . . 7 |- ( ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( v e. U /\ f e. v ) ) -> v e. { v | E. k e. A E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) } )
61		abid 2409	. . . . . . 7 |- ( v e. { v | E. k e. A E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) } <-> E. k e. A E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) )
62	60, 61	sylib 199	. . . . . 6 |- ( ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( v e. U /\ f e. v ) ) -> E. k e. A E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) )
63		rexim 2890	. . . . . 6 |- ( A. k e. A ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) -> ( E. k e. A E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> E. k e. A ( f ` k ) e. U. K ) )
64	55, 62, 63	sylc 62	. . . . 5 |- ( ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( v e. U /\ f e. v ) ) -> E. k e. A ( f ` k ) e. U. K )
65	28, 64	rexlimddv 2921	. . . 4 |- ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> E. k e. A ( f ` k ) e. U. K )
66		eldifn 3588	. . . . . . 7 |- ( ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> -. ( f ` k ) e. U. K )
67	66	ralimi 2818	. . . . . 6 |- ( A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> A. k e. A -. ( f ` k ) e. U. K )
68	67	ad2antll 733	. . . . 5 |- ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> A. k e. A -. ( f ` k ) e. U. K )
69		ralnex 2871	. . . . 5 |- ( A. k e. A -. ( f ` k ) e. U. K <-> -. E. k e. A ( f ` k ) e. U. K )
70	68, 69	sylib 199	. . . 4 |- ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> -. E. k e. A ( f ` k ) e. U. K )
71	65, 70	pm2.65da 578	. . 3 |- ( ph -> -. ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) )
72	71	nexdv 1771	. 2 |- ( ph -> -. E. f ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) )
73	10, 72	pm2.65i 176	1 |- -. ph

Syntax hints:   -. wn 3   -> wi 4   /\ wa 370   = wceq 1437   E.wex 1659   e. wcel 1868   {cab 2407   A.wral 2775   E.wrex 2776   {crab 2779   \ cdif 3433   i^i cin 3435   C_ wss 3436   ~Pcpw 3979   U.cuni 4216   |-> cmpt 4479   `'ccnv 4848   dom cdm 4849   ran crn 4850   "cima 4852   Fn wfn 5592   -->wf 5593   ` cfv 5597   |-> cmpt2 6303   X_cixp 7526   Fincfn 7573   cardccrd 8370   Compccmp 20385  UFLcufl 20899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-se 4809  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-isom 5606  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-om 6703  df-1st 6803  df-2nd 6804  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-1o 7186  df-oadd 7190  df-omul 7191  df-er 7367  df-map 7478  df-ixp 7527  df-en 7574  df-dom 7575  df-fin 7577  df-wdom 8076  df-card 8374  df-acn 8377  df-cmp 20386

This theorem is referenced by:  ptcmplem5  21055