Theorem konigthlem 8847

Description: Lemma for konigth 8848. (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 5812	. . . . . . . . 9 |- ( M ` i ) e. _V
2		fvex 5812	. . . . . . . . . . 11 |- ( ( f ` a ) ` i ) e. _V
3		eqid 2454	. . . . . . . . . . 11 |- ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) = ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) )
4	2, 3	fnmpti 5650	. . . . . . . . . 10 |- ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) Fn ( M ` i )
5	1	mptex 6060	. . . . . . . . . . . 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 5893	. . . . . . . . . . . 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 671	. . . . . . . . . . 11 |- ( i e. A -> ( D ` i ) = ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) )
9	8	fneq1d 5612	. . . . . . . . . 10 |- ( i e. A -> ( ( D ` i ) Fn ( M ` i ) <-> ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) Fn ( M ` i ) ) )
10	4, 9	mpbiri 233	. . . . . . . . 9 |- ( i e. A -> ( D ` i ) Fn ( M ` i ) )
11		fnrndomg 8817	. . . . . . . . 9 |- ( ( M ` i ) e. _V -> ( ( D ` i ) Fn ( M ` i ) -> ran ( D ` i ) ~<_ ( M ` i ) ) )
12	1, 10, 11	mpsyl 63	. . . . . . . 8 |- ( i e. A -> ran ( D ` i ) ~<_ ( M ` i ) )
13		domsdomtr 7559	. . . . . . . 8 |- ( ( ran ( D ` i ) ~<_ ( M ` i ) /\ ( M ` i ) ~< ( N ` i ) ) -> ran ( D ` i ) ~< ( N ` i ) )
14	12, 13	sylan 471	. . . . . . 7 |- ( ( i e. A /\ ( M ` i ) ~< ( N ` i ) ) -> ran ( D ` i ) ~< ( N ` i ) )
15		sdomdif 7572	. . . . . . 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 2818	. . . . 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 5812	. . . . . . 7 |- ( N ` i ) e. _V
20		difss 3594	. . . . . . 7 |- ( ( N ` i ) \ ran ( D ` i ) ) C_ ( N ` i )
21	19, 20	ssexi 4548	. . . . . 6 |- ( ( N ` i ) \ ran ( D ` i ) ) e. _V
22	18, 21	ac6c5 8766	. . . . 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 1731	. . . . . . 7 |- f = f
24		eldifi 3589	. . . . . . . . . . . . 13 |- ( ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( e ` i ) e. ( N ` i ) )
25		fvex 5812	. . . . . . . . . . . . . . 15 |- ( e ` i ) e. _V
26		konigth.5	. . . . . . . . . . . . . . . 16 |- E = ( i e. A |-> ( e ` i ) )
27	26	fvmpt2 5893	. . . . . . . . . . . . . . 15 |- ( ( i e. A /\ ( e ` i ) e. _V ) -> ( E ` i ) = ( e ` i ) )
28	25, 27	mpan2 671	. . . . . . . . . . . . . 14 |- ( i e. A -> ( E ` i ) = ( e ` i ) )
29	28	eleq1d 2523	. . . . . . . . . . . . 13 |- ( i e. A -> ( ( E ` i ) e. ( N ` i ) <-> ( e ` i ) e. ( N ` i ) ) )
30	24, 29	syl5ibr 221	. . . . . . . . . . . 12 |- ( i e. A -> ( ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( E ` i ) e. ( N ` i ) ) )
31	30	ralimia 2817	. . . . . . . . . . 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 5650	. . . . . . . . . . 11 |- E Fn A
33	31, 32	jctil 537	. . . . . . . . . 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 6060	. . . . . . . . . . . 12 |- ( i e. A |-> ( e ` i ) ) e. _V
35	26, 34	eqeltri 2538	. . . . . . . . . . 11 |- E e. _V
36	35	elixp 7383	. . . . . . . . . 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 212	. . . . . . . . 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 2553	. . . . . . . 8 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> E e. P )
40		foelrn 5974	. . . . . . . . . 10 |- ( ( f : S -onto-> P /\ E e. P ) -> E. a e. S E = ( f ` a ) )
41	40	expcom 435	. . . . . . . . 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 2532	. . . . . . . . . . . . . 14 |- ( a e. S <-> a e. U_ i e. A ( M ` i ) )
44		eliun 4286	. . . . . . . . . . . . . 14 |- ( a e. U_ i e. A ( M ` i ) <-> E. i e. A a e. ( M ` i ) )
45	43, 44	bitri 249	. . . . . . . . . . . . 13 |- ( a e. S <-> E. i e. A a e. ( M ` i ) )
46		nfra1 2810	. . . . . . . . . . . . . . 15 |- F/ i A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) )
47		nfv 1674	. . . . . . . . . . . . . . 15 |- F/ i E = ( f ` a )
48	46, 47	nfan 1866	. . . . . . . . . . . . . 14 |- F/ i ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) )
49		nfv 1674	. . . . . . . . . . . . . 14 |- F/ i -. f = f
50	28	ad2antrl 727	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( E ` i ) = ( e ` i ) )
51		fveq1 5801	. . . . . . . . . . . . . . . . . . . . 21 |- ( E = ( f ` a ) -> ( E ` i ) = ( ( f ` a ) ` i ) )
52	8	fveq1d 5804	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( i e. A -> ( ( D ` i ) ` a ) = ( ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) ` a ) )
53	3	fvmpt2 5893	. . . . . . . . . . . . . . . . . . . . . . . 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 671	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a e. ( M ` i ) -> ( ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) ` a ) = ( ( f ` a ) ` i ) )
55	52, 54	sylan9eq 2515	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( i e. A /\ a e. ( M ` i ) ) -> ( ( D ` i ) ` a ) = ( ( f ` a ) ` i ) )
56	55	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i e. A /\ a e. ( M ` i ) ) -> ( ( f ` a ) ` i ) = ( ( D ` i ) ` a ) )
57	51, 56	sylan9eq 2515	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( E ` i ) = ( ( D ` i ) ` a ) )
58	50, 57	eqtr3d 2497	. . . . . . . . . . . . . . . . . . 19 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( e ` i ) = ( ( D ` i ) ` a ) )
59		fnfvelrn 5952	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( D ` i ) Fn ( M ` i ) /\ a e. ( M ` i ) ) -> ( ( D ` i ) ` a ) e. ran ( D ` i ) )
60	10, 59	sylan 471	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. A /\ a e. ( M ` i ) ) -> ( ( D ` i ) ` a ) e. ran ( D ` i ) )
61	60	adantl 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( ( D ` i ) ` a ) e. ran ( D ` i ) )
62	58, 61	eqeltrd 2542	. . . . . . . . . . . . . . . . . 18 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( e ` i ) e. ran ( D ` i ) )
63	62	3adant1 1006	. . . . . . . . . . . . . . . . 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 988	. . . . . . . . . . . . . . . . . 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 1016	. . . . . . . . . . . . . . . . . 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 2894	. . . . . . . . . . . . . . . . . . 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 3590	. . . . . . . . . . . . . . . . . . 19 |- ( ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> -. ( e ` i ) e. ran ( D ` i ) )
68	66, 67	syl6 33	. . . . . . . . . . . . . . . . . 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 60	. . . . . . . . . . . . . . . . 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 174	. . . . . . . . . . . . . . . 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 1190	. . . . . . . . . . . . . . 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 436	. . . . . . . . . . . . . 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 2944	. . . . . . . . . . . . 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 217	. . . . . . . . . . . 12 |- ( ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) ) -> ( a e. S -> -. f = f ) )
75	74	ex 434	. . . . . . . . . . 11 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( E = ( f ` a ) -> ( a e. S -> -. f = f ) ) )
76	75	com23 78	. . . . . . . . . 10 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( a e. S -> ( E = ( f ` a ) -> -. f = f ) ) )
77	76	rexlimdv 2946	. . . . . . . . 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 72	. . . . . . . 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 118	. . . . . 6 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> -. f : S -onto-> P )
81	80	exlimiv 1689	. . . . 5 |- ( E. e A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> -. f : S -onto-> P )
82	17, 22, 81	3syl 20	. . . 4 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> -. f : S -onto-> P )
83	82	nexdv 1823	. . 3 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> -. E. f f : S -onto-> P )
84	1	0dom 7554	. . . . . . . 8 |- (/) ~<_ ( M ` i )
85		domsdomtr 7559	. . . . . . . 8 |- ( ( (/) ~<_ ( M ` i ) /\ ( M ` i ) ~< ( N ` i ) ) -> (/) ~< ( N ` i ) )
86	84, 85	mpan 670	. . . . . . 7 |- ( ( M ` i ) ~< ( N ` i ) -> (/) ~< ( N ` i ) )
87	19	0sdom 7555	. . . . . . 7 |- ( (/) ~< ( N ` i ) <-> ( N ` i ) =/= (/) )
88	86, 87	sylib 196	. . . . . 6 |- ( ( M ` i ) ~< ( N ` i ) -> ( N ` i ) =/= (/) )
89	88	ralimi 2819	. . . . 5 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> A. i e. A ( N ` i ) =/= (/) )
90	38	neeq1i 2737	. . . . . 6 |- ( P =/= (/) <-> X_ i e. A ( N ` i ) =/= (/) )
91	19	rgenw 2901	. . . . . . . . 9 |- A. i e. A ( N ` i ) e. _V
92		ixpexg 7400	. . . . . . . . 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 2538	. . . . . . 7 |- P e. _V
95	94	0sdom 7555	. . . . . 6 |- ( (/) ~< P <-> P =/= (/) )
96	18, 19	ac9 8767	. . . . . 6 |- ( A. i e. A ( N ` i ) =/= (/) <-> X_ i e. A ( N ` i ) =/= (/) )
97	90, 95, 96	3bitr4i 277	. . . . 5 |- ( (/) ~< P <-> A. i e. A ( N ` i ) =/= (/) )
98	89, 97	sylibr 212	. . . 4 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> (/) ~< P )
99	18, 1	iunex 6670	. . . . . . 7 |- U_ i e. A ( M ` i ) e. _V
100	42, 99	eqeltri 2538	. . . . . 6 |- S e. _V
101		domtri 8835	. . . . . 6 |- ( ( P e. _V /\ S e. _V ) -> ( P ~<_ S <-> -. S ~< P ) )
102	94, 100, 101	mp2an 672	. . . . 5 |- ( P ~<_ S <-> -. S ~< P )
103	102	biimpri 206	. . . 4 |- ( -. S ~< P -> P ~<_ S )
104		fodomr 7575	. . . 4 |- ( ( (/) ~< P /\ P ~<_ S ) -> E. f f : S -onto-> P )
105	98, 103, 104	syl2an 477	. . 3 |- ( ( A. i e. A ( M ` i ) ~< ( N ` i ) /\ -. S ~< P ) -> E. f f : S -onto-> P )
106	83, 105	mtand 659	. 2 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> -. -. S ~< P )
107	106	notnotrd 113	1 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> S ~< P )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   = wceq 1370   E.wex 1587   e. wcel 1758   =/= wne 2648   A.wral 2799   E.wrex 2800   _Vcvv 3078   \ cdif 3436   (/)c0 3748   U_ciun 4282   class class class wbr 4403   |-> cmpt 4461   ran crn 4952   Fn wfn 5524   -onto->wfo 5527   ` cfv 5529   X_cixp 7376   ~<_ cdom 7421   ~< csdm 7422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4514  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485  ax-ac2 8747

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-reu 2806  df-rmo 2807  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-pss 3455  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-tp 3993  df-op 3995  df-uni 4203  df-int 4240  df-iun 4284  df-br 4404  df-opab 4462  df-mpt 4463  df-tr 4497  df-eprel 4743  df-id 4747  df-po 4752  df-so 4753  df-fr 4790  df-se 4791  df-we 4792  df-ord 4833  df-on 4834  df-suc 4836  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-isom 5538  df-riota 6164  df-ov 6206  df-oprab 6207  df-mpt2 6208  df-1st 6690  df-2nd 6691  df-recs 6945  df-er 7214  df-map 7329  df-ixp 7377  df-en 7424  df-dom 7425  df-sdom 7426  df-card 8224  df-acn 8227  df-ac 8401

This theorem is referenced by:  konigth  8848