Theorem konigthlem 8990

Description: Lemma for konigth 8991. (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 5873	. . . . . . . . 9 |- ( M ` i ) e. _V
2		fvex 5873	. . . . . . . . . . 11 |- ( ( f ` a ) ` i ) e. _V
3		eqid 2450	. . . . . . . . . . 11 |- ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) = ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) )
4	2, 3	fnmpti 5704	. . . . . . . . . 10 |- ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) Fn ( M ` i )
5	1	mptex 6134	. . . . . . . . . . . 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 5955	. . . . . . . . . . . 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 676	. . . . . . . . . . 11 |- ( i e. A -> ( D ` i ) = ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) )
9	8	fneq1d 5664	. . . . . . . . . 10 |- ( i e. A -> ( ( D ` i ) Fn ( M ` i ) <-> ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) Fn ( M ` i ) ) )
10	4, 9	mpbiri 237	. . . . . . . . 9 |- ( i e. A -> ( D ` i ) Fn ( M ` i ) )
11		fnrndomg 8960	. . . . . . . . 9 |- ( ( M ` i ) e. _V -> ( ( D ` i ) Fn ( M ` i ) -> ran ( D ` i ) ~<_ ( M ` i ) ) )
12	1, 10, 11	mpsyl 65	. . . . . . . 8 |- ( i e. A -> ran ( D ` i ) ~<_ ( M ` i ) )
13		domsdomtr 7704	. . . . . . . 8 |- ( ( ran ( D ` i ) ~<_ ( M ` i ) /\ ( M ` i ) ~< ( N ` i ) ) -> ran ( D ` i ) ~< ( N ` i ) )
14	12, 13	sylan 474	. . . . . . 7 |- ( ( i e. A /\ ( M ` i ) ~< ( N ` i ) ) -> ran ( D ` i ) ~< ( N ` i ) )
15		sdomdif 7717	. . . . . . 7 |- ( ran ( D ` i ) ~< ( N ` i ) -> ( ( N ` i ) \ ran ( D ` i ) ) =/= (/) )
16	14, 15	syl 17	. . . . . 6 |- ( ( i e. A /\ ( M ` i ) ~< ( N ` i ) ) -> ( ( N ` i ) \ ran ( D ` i ) ) =/= (/) )
17	16	ralimiaa 2779	. . . . 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 5873	. . . . . . 7 |- ( N ` i ) e. _V
20		difss 3559	. . . . . . 7 |- ( ( N ` i ) \ ran ( D ` i ) ) C_ ( N ` i )
21	19, 20	ssexi 4547	. . . . . 6 |- ( ( N ` i ) \ ran ( D ` i ) ) e. _V
22	18, 21	ac6c5 8909	. . . . 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 1854	. . . . . . 7 |- f = f
24		eldifi 3554	. . . . . . . . . . . . 13 |- ( ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( e ` i ) e. ( N ` i ) )
25		fvex 5873	. . . . . . . . . . . . . . 15 |- ( e ` i ) e. _V
26		konigth.5	. . . . . . . . . . . . . . . 16 |- E = ( i e. A |-> ( e ` i ) )
27	26	fvmpt2 5955	. . . . . . . . . . . . . . 15 |- ( ( i e. A /\ ( e ` i ) e. _V ) -> ( E ` i ) = ( e ` i ) )
28	25, 27	mpan2 676	. . . . . . . . . . . . . 14 |- ( i e. A -> ( E ` i ) = ( e ` i ) )
29	28	eleq1d 2512	. . . . . . . . . . . . 13 |- ( i e. A -> ( ( E ` i ) e. ( N ` i ) <-> ( e ` i ) e. ( N ` i ) ) )
30	24, 29	syl5ibr 225	. . . . . . . . . . . 12 |- ( i e. A -> ( ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( E ` i ) e. ( N ` i ) ) )
31	30	ralimia 2778	. . . . . . . . . . 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 5704	. . . . . . . . . . 11 |- E Fn A
33	31, 32	jctil 540	. . . . . . . . . 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 6134	. . . . . . . . . . . 12 |- ( i e. A |-> ( e ` i ) ) e. _V
35	26, 34	eqeltri 2524	. . . . . . . . . . 11 |- E e. _V
36	35	elixp 7526	. . . . . . . . . 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 216	. . . . . . . . 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 2539	. . . . . . . 8 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> E e. P )
40		foelrn 6039	. . . . . . . . . 10 |- ( ( f : S -onto-> P /\ E e. P ) -> E. a e. S E = ( f ` a ) )
41	40	expcom 437	. . . . . . . . 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 2520	. . . . . . . . . . . . . 14 |- ( a e. S <-> a e. U_ i e. A ( M ` i ) )
44		eliun 4282	. . . . . . . . . . . . . 14 |- ( a e. U_ i e. A ( M ` i ) <-> E. i e. A a e. ( M ` i ) )
45	43, 44	bitri 253	. . . . . . . . . . . . 13 |- ( a e. S <-> E. i e. A a e. ( M ` i ) )
46		nfra1 2768	. . . . . . . . . . . . . . 15 |- F/ i A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) )
47		nfv 1760	. . . . . . . . . . . . . . 15 |- F/ i E = ( f ` a )
48	46, 47	nfan 2010	. . . . . . . . . . . . . 14 |- F/ i ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) )
49		nfv 1760	. . . . . . . . . . . . . 14 |- F/ i -. f = f
50	28	ad2antrl 733	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( E ` i ) = ( e ` i ) )
51		fveq1 5862	. . . . . . . . . . . . . . . . . . . . 21 |- ( E = ( f ` a ) -> ( E ` i ) = ( ( f ` a ) ` i ) )
52	8	fveq1d 5865	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( i e. A -> ( ( D ` i ) ` a ) = ( ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) ` a ) )
53	3	fvmpt2 5955	. . . . . . . . . . . . . . . . . . . . . . . 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 676	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a e. ( M ` i ) -> ( ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) ` a ) = ( ( f ` a ) ` i ) )
55	52, 54	sylan9eq 2504	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( i e. A /\ a e. ( M ` i ) ) -> ( ( D ` i ) ` a ) = ( ( f ` a ) ` i ) )
56	55	eqcomd 2456	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i e. A /\ a e. ( M ` i ) ) -> ( ( f ` a ) ` i ) = ( ( D ` i ) ` a ) )
57	51, 56	sylan9eq 2504	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( E ` i ) = ( ( D ` i ) ` a ) )
58	50, 57	eqtr3d 2486	. . . . . . . . . . . . . . . . . . 19 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( e ` i ) = ( ( D ` i ) ` a ) )
59		fnfvelrn 6017	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( D ` i ) Fn ( M ` i ) /\ a e. ( M ` i ) ) -> ( ( D ` i ) ` a ) e. ran ( D ` i ) )
60	10, 59	sylan 474	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. A /\ a e. ( M ` i ) ) -> ( ( D ` i ) ` a ) e. ran ( D ` i ) )
61	60	adantl 468	. . . . . . . . . . . . . . . . . . 19 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( ( D ` i ) ` a ) e. ran ( D ` i ) )
62	58, 61	eqeltrd 2528	. . . . . . . . . . . . . . . . . 18 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( e ` i ) e. ran ( D ` i ) )
63	62	3adant1 1025	. . . . . . . . . . . . . . . . 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 1007	. . . . . . . . . . . . . . . . . 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 1035	. . . . . . . . . . . . . . . . . 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 2753	. . . . . . . . . . . . . . . . . . 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 3555	. . . . . . . . . . . . . . . . . . 19 |- ( ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> -. ( e ` i ) e. ran ( D ` i ) )
68	66, 67	syl6 34	. . . . . . . . . . . . . . . . . 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 62	. . . . . . . . . . . . . . . . 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 178	. . . . . . . . . . . . . . . 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 1209	. . . . . . . . . . . . . . 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	expd 438	. . . . . . . . . . . . . 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 2870	. . . . . . . . . . . . 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 221	. . . . . . . . . . . 12 |- ( ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) ) -> ( a e. S -> -. f = f ) )
75	74	ex 436	. . . . . . . . . . 11 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( E = ( f ` a ) -> ( a e. S -> -. f = f ) ) )
76	75	com23 81	. . . . . . . . . 10 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( a e. S -> ( E = ( f ` a ) -> -. f = f ) ) )
77	76	rexlimdv 2876	. . . . . . . . 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 74	. . . . . . . 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 122	. . . . . 6 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> -. f : S -onto-> P )
81	80	exlimiv 1775	. . . . 5 |- ( E. e A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> -. f : S -onto-> P )
82	17, 22, 81	3syl 18	. . . 4 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> -. f : S -onto-> P )
83	82	nexdv 1781	. . 3 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> -. E. f f : S -onto-> P )
84	1	0dom 7699	. . . . . . . 8 |- (/) ~<_ ( M ` i )
85		domsdomtr 7704	. . . . . . . 8 |- ( ( (/) ~<_ ( M ` i ) /\ ( M ` i ) ~< ( N ` i ) ) -> (/) ~< ( N ` i ) )
86	84, 85	mpan 675	. . . . . . 7 |- ( ( M ` i ) ~< ( N ` i ) -> (/) ~< ( N ` i ) )
87	19	0sdom 7700	. . . . . . 7 |- ( (/) ~< ( N ` i ) <-> ( N ` i ) =/= (/) )
88	86, 87	sylib 200	. . . . . 6 |- ( ( M ` i ) ~< ( N ` i ) -> ( N ` i ) =/= (/) )
89	88	ralimi 2780	. . . . 5 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> A. i e. A ( N ` i ) =/= (/) )
90	38	neeq1i 2687	. . . . . 6 |- ( P =/= (/) <-> X_ i e. A ( N ` i ) =/= (/) )
91	19	rgenw 2748	. . . . . . . . 9 |- A. i e. A ( N ` i ) e. _V
92		ixpexg 7543	. . . . . . . . 9 |- ( A. i e. A ( N ` i ) e. _V -> X_ i e. A ( N ` i ) e. _V )
93	91, 92	ax-mp 5	. . . . . . . 8 |- X_ i e. A ( N ` i ) e. _V
94	38, 93	eqeltri 2524	. . . . . . 7 |- P e. _V
95	94	0sdom 7700	. . . . . 6 |- ( (/) ~< P <-> P =/= (/) )
96	18, 19	ac9 8910	. . . . . 6 |- ( A. i e. A ( N ` i ) =/= (/) <-> X_ i e. A ( N ` i ) =/= (/) )
97	90, 95, 96	3bitr4i 281	. . . . 5 |- ( (/) ~< P <-> A. i e. A ( N ` i ) =/= (/) )
98	89, 97	sylibr 216	. . . 4 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> (/) ~< P )
99	18, 1	iunex 6770	. . . . . . 7 |- U_ i e. A ( M ` i ) e. _V
100	42, 99	eqeltri 2524	. . . . . 6 |- S e. _V
101		domtri 8978	. . . . . 6 |- ( ( P e. _V /\ S e. _V ) -> ( P ~<_ S <-> -. S ~< P ) )
102	94, 100, 101	mp2an 677	. . . . 5 |- ( P ~<_ S <-> -. S ~< P )
103	102	biimpri 210	. . . 4 |- ( -. S ~< P -> P ~<_ S )
104		fodomr 7720	. . . 4 |- ( ( (/) ~< P /\ P ~<_ S ) -> E. f f : S -onto-> P )
105	98, 103, 104	syl2an 480	. . 3 |- ( ( A. i e. A ( M ` i ) ~< ( N ` i ) /\ -. S ~< P ) -> E. f f : S -onto-> P )
106	83, 105	mtand 664	. 2 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> -. -. S ~< P )
107	106	notnotrd 117	1 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> S ~< P )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   /\ wa 371   /\ w3a 984   = wceq 1443   E.wex 1662   e. wcel 1886   =/= wne 2621   A.wral 2736   E.wrex 2737   _Vcvv 3044   \ cdif 3400   (/)c0 3730   U_ciun 4277   class class class wbr 4401   |-> cmpt 4460   ran crn 4834   Fn wfn 5576   -onto->wfo 5579   ` cfv 5581   X_cixp 7519   ~<_ cdom 7564   ~< csdm 7565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-ac2 8890

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-se 4793  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-isom 5590  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-er 7360  df-map 7471  df-ixp 7520  df-en 7567  df-dom 7568  df-sdom 7569  df-card 8370  df-acn 8373  df-ac 8544

This theorem is referenced by:  konigth  8991