Theorem konigthlem 8399

Description: Lemma for konigth 8400. (Contributed by Mario Carneiro, 22-Feb-2013.)

Hypotheses

Ref	Expression
konigth.1	|- A e. _V
konigth.2	|- S = U_ i e. A ( M ` i )
konigth.3	|- P = X_ i e. A ( N ` i )
konigth.4	|- D = ( i e. A |-> ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) )
konigth.5	|- E = ( i e. A |-> ( e ` i ) )

Assertion

Ref	Expression
konigthlem	|- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> S ~< P )

Distinct variable groups:   A, a, e, f, i   D, a, e   E, a, i   M, a, f   N, a, e, f   P, a, e, f   S, a, e, f

Allowed substitution hints:   D( f, i)   P( i)   S( i)   E( e, f)   M( e, i)   N( i)

Proof of Theorem konigthlem

Step	Hyp	Ref	Expression
1		fvex 5701	. . . . . . . . 9 |- ( M ` i ) e. _V
2		fvex 5701	. . . . . . . . . . 11 |- ( ( f ` a ) ` i ) e. _V
3		eqid 2404	. . . . . . . . . . 11 |- ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) = ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) )
4	2, 3	fnmpti 5532	. . . . . . . . . 10 |- ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) Fn ( M ` i )
5	1	mptex 5925	. . . . . . . . . . . 12 |- ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) e. _V
6		konigth.4	. . . . . . . . . . . . 13 |- D = ( i e. A |-> ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) )
7	6	fvmpt2 5771	. . . . . . . . . . . 12 |- ( ( i e. A /\ ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) e. _V ) -> ( D ` i ) = ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) )
8	5, 7	mpan2 653	. . . . . . . . . . 11 |- ( i e. A -> ( D ` i ) = ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) )
9	8	fneq1d 5495	. . . . . . . . . 10 |- ( i e. A -> ( ( D ` i ) Fn ( M ` i ) <-> ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) Fn ( M ` i ) ) )
10	4, 9	mpbiri 225	. . . . . . . . 9 |- ( i e. A -> ( D ` i ) Fn ( M ` i ) )
11		fnrndomg 8369	. . . . . . . . 9 |- ( ( M ` i ) e. _V -> ( ( D ` i ) Fn ( M ` i ) -> ran ( D ` i ) ~<_ ( M ` i ) ) )
12	1, 10, 11	mpsyl 61	. . . . . . . 8 |- ( i e. A -> ran ( D ` i ) ~<_ ( M ` i ) )
13		domsdomtr 7201	. . . . . . . 8 |- ( ( ran ( D ` i ) ~<_ ( M ` i ) /\ ( M ` i ) ~< ( N ` i ) ) -> ran ( D ` i ) ~< ( N ` i ) )
14	12, 13	sylan 458	. . . . . . 7 |- ( ( i e. A /\ ( M ` i ) ~< ( N ` i ) ) -> ran ( D ` i ) ~< ( N ` i ) )
15		sdomdif 7214	. . . . . . 7 |- ( ran ( D ` i ) ~< ( N ` i ) -> ( ( N ` i ) \ ran ( D ` i ) ) =/= (/) )
16	14, 15	syl 16	. . . . . 6 |- ( ( i e. A /\ ( M ` i ) ~< ( N ` i ) ) -> ( ( N ` i ) \ ran ( D ` i ) ) =/= (/) )
17	16	ralimiaa 2740	. . . . 5 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> A. i e. A ( ( N ` i ) \ ran ( D ` i ) ) =/= (/) )
18		konigth.1	. . . . . 6 |- A e. _V
19		fvex 5701	. . . . . . 7 |- ( N ` i ) e. _V
20		difss 3434	. . . . . . 7 |- ( ( N ` i ) \ ran ( D ` i ) ) C_ ( N ` i )
21	19, 20	ssexi 4308	. . . . . 6 |- ( ( N ` i ) \ ran ( D ` i ) ) e. _V
22	18, 21	ac6c5 8318	. . . . 5 |- ( A. i e. A ( ( N ` i ) \ ran ( D ` i ) ) =/= (/) -> E. e A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) )
23		equid 1684	. . . . . . 7 |- f = f
24		eldifi 3429	. . . . . . . . . . . . 13 |- ( ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( e ` i ) e. ( N ` i ) )
25		fvex 5701	. . . . . . . . . . . . . . 15 |- ( e ` i ) e. _V
26		konigth.5	. . . . . . . . . . . . . . . 16 |- E = ( i e. A |-> ( e ` i ) )
27	26	fvmpt2 5771	. . . . . . . . . . . . . . 15 |- ( ( i e. A /\ ( e ` i ) e. _V ) -> ( E ` i ) = ( e ` i ) )
28	25, 27	mpan2 653	. . . . . . . . . . . . . 14 |- ( i e. A -> ( E ` i ) = ( e ` i ) )
29	28	eleq1d 2470	. . . . . . . . . . . . 13 |- ( i e. A -> ( ( E ` i ) e. ( N ` i ) <-> ( e ` i ) e. ( N ` i ) ) )
30	24, 29	syl5ibr 213	. . . . . . . . . . . 12 |- ( i e. A -> ( ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( E ` i ) e. ( N ` i ) ) )
31	30	ralimia 2739	. . . . . . . . . . 11 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> A. i e. A ( E ` i ) e. ( N ` i ) )
32	25, 26	fnmpti 5532	. . . . . . . . . . 11 |- E Fn A
33	31, 32	jctil 524	. . . . . . . . . 10 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( E Fn A /\ A. i e. A ( E ` i ) e. ( N ` i ) ) )
34	18	mptex 5925	. . . . . . . . . . . 12 |- ( i e. A |-> ( e ` i ) ) e. _V
35	26, 34	eqeltri 2474	. . . . . . . . . . 11 |- E e. _V
36	35	elixp 7028	. . . . . . . . . 10 |- ( E e. X_ i e. A ( N ` i ) <-> ( E Fn A /\ A. i e. A ( E ` i ) e. ( N ` i ) ) )
37	33, 36	sylibr 204	. . . . . . . . 9 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> E e. X_ i e. A ( N ` i ) )
38		konigth.3	. . . . . . . . 9 |- P = X_ i e. A ( N ` i )
39	37, 38	syl6eleqr 2495	. . . . . . . 8 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> E e. P )
40		foelrn 5847	. . . . . . . . . 10 |- ( ( f : S -onto-> P /\ E e. P ) -> E. a e. S E = ( f ` a ) )
41	40	expcom 425	. . . . . . . . 9 |- ( E e. P -> ( f : S -onto-> P -> E. a e. S E = ( f ` a ) ) )
42		konigth.2	. . . . . . . . . . . . . . 15 |- S = U_ i e. A ( M ` i )
43	42	eleq2i 2468	. . . . . . . . . . . . . 14 |- ( a e. S <-> a e. U_ i e. A ( M ` i ) )
44		eliun 4057	. . . . . . . . . . . . . 14 |- ( a e. U_ i e. A ( M ` i ) <-> E. i e. A a e. ( M ` i ) )
45	43, 44	bitri 241	. . . . . . . . . . . . 13 |- ( a e. S <-> E. i e. A a e. ( M ` i ) )
46		nfra1 2716	. . . . . . . . . . . . . . 15 |- F/ i A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) )
47		nfv 1626	. . . . . . . . . . . . . . 15 |- F/ i E = ( f ` a )
48	46, 47	nfan 1842	. . . . . . . . . . . . . 14 |- F/ i ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) )
49		nfv 1626	. . . . . . . . . . . . . 14 |- F/ i -. f = f
50	28	ad2antrl 709	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( E ` i ) = ( e ` i ) )
51		fveq1 5686	. . . . . . . . . . . . . . . . . . . . 21 |- ( E = ( f ` a ) -> ( E ` i ) = ( ( f ` a ) ` i ) )
52	8	fveq1d 5689	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( i e. A -> ( ( D ` i ) ` a ) = ( ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) ` a ) )
53	3	fvmpt2 5771	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( a e. ( M ` i ) /\ ( ( f ` a ) ` i ) e. _V ) -> ( ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) ` a ) = ( ( f ` a ) ` i ) )
54	2, 53	mpan2 653	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a e. ( M ` i ) -> ( ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) ` a ) = ( ( f ` a ) ` i ) )
55	52, 54	sylan9eq 2456	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( i e. A /\ a e. ( M ` i ) ) -> ( ( D ` i ) ` a ) = ( ( f ` a ) ` i ) )
56	55	eqcomd 2409	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i e. A /\ a e. ( M ` i ) ) -> ( ( f ` a ) ` i ) = ( ( D ` i ) ` a ) )
57	51, 56	sylan9eq 2456	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( E ` i ) = ( ( D ` i ) ` a ) )
58	50, 57	eqtr3d 2438	. . . . . . . . . . . . . . . . . . 19 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( e ` i ) = ( ( D ` i ) ` a ) )
59		fnfvelrn 5826	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( D ` i ) Fn ( M ` i ) /\ a e. ( M ` i ) ) -> ( ( D ` i ) ` a ) e. ran ( D ` i ) )
60	10, 59	sylan 458	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. A /\ a e. ( M ` i ) ) -> ( ( D ` i ) ` a ) e. ran ( D ` i ) )
61	60	adantl 453	. . . . . . . . . . . . . . . . . . 19 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( ( D ` i ) ` a ) e. ran ( D ` i ) )
62	58, 61	eqeltrd 2478	. . . . . . . . . . . . . . . . . 18 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( e ` i ) e. ran ( D ` i ) )
63	62	3adant1 975	. . . . . . . . . . . . . . . . 17 |- ( ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( e ` i ) e. ran ( D ` i ) )
64		simp1 957	. . . . . . . . . . . . . . . . . 18 |- ( ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) )
65		simp3l 985	. . . . . . . . . . . . . . . . . 18 |- ( ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> i e. A )
66		rsp 2726	. . . . . . . . . . . . . . . . . . 19 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( i e. A -> ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) ) )
67		eldifn 3430	. . . . . . . . . . . . . . . . . . 19 |- ( ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> -. ( e ` i ) e. ran ( D ` i ) )
68	66, 67	syl6 31	. . . . . . . . . . . . . . . . . 18 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( i e. A -> -. ( e ` i ) e. ran ( D ` i ) ) )
69	64, 65, 68	sylc 58	. . . . . . . . . . . . . . . . 17 |- ( ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> -. ( e ` i ) e. ran ( D ` i ) )
70	63, 69	pm2.21dd 101	. . . . . . . . . . . . . . . 16 |- ( ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> -. f = f )
71	70	3expia 1155	. . . . . . . . . . . . . . 15 |- ( ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) ) -> ( ( i e. A /\ a e. ( M ` i ) ) -> -. f = f ) )
72	71	exp3a 426	. . . . . . . . . . . . . 14 |- ( ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) ) -> ( i e. A -> ( a e. ( M ` i ) -> -. f = f ) ) )
73	48, 49, 72	rexlimd 2787	. . . . . . . . . . . . 13 |- ( ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) ) -> ( E. i e. A a e. ( M ` i ) -> -. f = f ) )
74	45, 73	syl5bi 209	. . . . . . . . . . . 12 |- ( ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) ) -> ( a e. S -> -. f = f ) )
75	74	ex 424	. . . . . . . . . . 11 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( E = ( f ` a ) -> ( a e. S -> -. f = f ) ) )
76	75	com23 74	. . . . . . . . . 10 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( a e. S -> ( E = ( f ` a ) -> -. f = f ) ) )
77	76	rexlimdv 2789	. . . . . . . . 9 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( E. a e. S E = ( f ` a ) -> -. f = f ) )
78	41, 77	syl9r 69	. . . . . . . 8 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( E e. P -> ( f : S -onto-> P -> -. f = f ) ) )
79	39, 78	mpd 15	. . . . . . 7 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( f : S -onto-> P -> -. f = f ) )
80	23, 79	mt2i 112	. . . . . 6 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> -. f : S -onto-> P )
81	80	exlimiv 1641	. . . . 5 |- ( E. e A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> -. f : S -onto-> P )
82	17, 22, 81	3syl 19	. . . 4 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> -. f : S -onto-> P )
83	82	nexdv 1937	. . 3 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> -. E. f f : S -onto-> P )
84	1	0dom 7196	. . . . . . . 8 |- (/) ~<_ ( M ` i )
85		domsdomtr 7201	. . . . . . . 8 |- ( ( (/) ~<_ ( M ` i ) /\ ( M ` i ) ~< ( N ` i ) ) -> (/) ~< ( N ` i ) )
86	84, 85	mpan 652	. . . . . . 7 |- ( ( M ` i ) ~< ( N ` i ) -> (/) ~< ( N ` i ) )
87	19	0sdom 7197	. . . . . . 7 |- ( (/) ~< ( N ` i ) <-> ( N ` i ) =/= (/) )
88	86, 87	sylib 189	. . . . . 6 |- ( ( M ` i ) ~< ( N ` i ) -> ( N ` i ) =/= (/) )
89	88	ralimi 2741	. . . . 5 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> A. i e. A ( N ` i ) =/= (/) )
90	38	neeq1i 2577	. . . . . 6 |- ( P =/= (/) <-> X_ i e. A ( N ` i ) =/= (/) )
91	19	rgenw 2733	. . . . . . . . 9 |- A. i e. A ( N ` i ) e. _V
92		ixpexg 7045	. . . . . . . . 9 |- ( A. i e. A ( N ` i ) e. _V -> X_ i e. A ( N ` i ) e. _V )
93	91, 92	ax-mp 8	. . . . . . . 8 |- X_ i e. A ( N ` i ) e. _V
94	38, 93	eqeltri 2474	. . . . . . 7 |- P e. _V
95	94	0sdom 7197	. . . . . 6 |- ( (/) ~< P <-> P =/= (/) )
96	18, 19	ac9 8319	. . . . . 6 |- ( A. i e. A ( N ` i ) =/= (/) <-> X_ i e. A ( N ` i ) =/= (/) )
97	90, 95, 96	3bitr4i 269	. . . . 5 |- ( (/) ~< P <-> A. i e. A ( N ` i ) =/= (/) )
98	89, 97	sylibr 204	. . . 4 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> (/) ~< P )
99	18, 1	iunex 5950	. . . . . . 7 |- U_ i e. A ( M ` i ) e. _V
100	42, 99	eqeltri 2474	. . . . . 6 |- S e. _V
101		domtri 8387	. . . . . 6 |- ( ( P e. _V /\ S e. _V ) -> ( P ~<_ S <-> -. S ~< P ) )
102	94, 100, 101	mp2an 654	. . . . 5 |- ( P ~<_ S <-> -. S ~< P )
103	102	biimpri 198	. . . 4 |- ( -. S ~< P -> P ~<_ S )
104		fodomr 7217	. . . 4 |- ( ( (/) ~< P /\ P ~<_ S ) -> E. f f : S -onto-> P )
105	98, 103, 104	syl2an 464	. . 3 |- ( ( A. i e. A ( M ` i ) ~< ( N ` i ) /\ -. S ~< P ) -> E. f f : S -onto-> P )
106	83, 105	mtand 641	. 2 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> -. -. S ~< P )
107	106	notnotrd 107	1 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> S ~< P )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   E.wex 1547   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916   \ cdif 3277   (/)c0 3588   U_ciun 4053   class class class wbr 4172   e. cmpt 4226   ran crn 4838   Fn wfn 5408   -onto->wfo 5411   ` cfv 5413   X_cixp 7022   ~<_ cdom 7066   ~< csdm 7067

This theorem is referenced by:  konigth  8400

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-ac2 8299

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-suc 4547  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-er 6864  df-map 6979  df-ixp 7023  df-en 7069  df-dom 7070  df-sdom 7071  df-card 7782  df-acn 7785  df-ac 7953