Theorem konigthlem 8728

Description: Lemma for konigth 8729. (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 5698	. . . . . . . . 9 |- ( M ` i ) e. _V
2		fvex 5698	. . . . . . . . . . 11 |- ( ( f ` a ) ` i ) e. _V
3		eqid 2441	. . . . . . . . . . 11 |- ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) = ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) )
4	2, 3	fnmpti 5536	. . . . . . . . . 10 |- ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) Fn ( M ` i )
5	1	mptex 5945	. . . . . . . . . . . 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 5778	. . . . . . . . . . . 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 666	. . . . . . . . . . 11 |- ( i e. A -> ( D ` i ) = ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) )
9	8	fneq1d 5498	. . . . . . . . . 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 8698	. . . . . . . . 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 7442	. . . . . . . 8 |- ( ( ran ( D ` i ) ~<_ ( M ` i ) /\ ( M ` i ) ~< ( N ` i ) ) -> ran ( D ` i ) ~< ( N ` i ) )
14	12, 13	sylan 468	. . . . . . 7 |- ( ( i e. A /\ ( M ` i ) ~< ( N ` i ) ) -> ran ( D ` i ) ~< ( N ` i ) )
15		sdomdif 7455	. . . . . . 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 2788	. . . . 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 5698	. . . . . . 7 |- ( N ` i ) e. _V
20		difss 3480	. . . . . . 7 |- ( ( N ` i ) \ ran ( D ` i ) ) C_ ( N ` i )
21	19, 20	ssexi 4434	. . . . . 6 |- ( ( N ` i ) \ ran ( D ` i ) ) e. _V
22	18, 21	ac6c5 8647	. . . . 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 1734	. . . . . . 7 |- f = f
24		eldifi 3475	. . . . . . . . . . . . 13 |- ( ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( e ` i ) e. ( N ` i ) )
25		fvex 5698	. . . . . . . . . . . . . . 15 |- ( e ` i ) e. _V
26		konigth.5	. . . . . . . . . . . . . . . 16 |- E = ( i e. A |-> ( e ` i ) )
27	26	fvmpt2 5778	. . . . . . . . . . . . . . 15 |- ( ( i e. A /\ ( e ` i ) e. _V ) -> ( E ` i ) = ( e ` i ) )
28	25, 27	mpan2 666	. . . . . . . . . . . . . 14 |- ( i e. A -> ( E ` i ) = ( e ` i ) )
29	28	eleq1d 2507	. . . . . . . . . . . . 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 2787	. . . . . . . . . . 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 5536	. . . . . . . . . . 11 |- E Fn A
33	31, 32	jctil 534	. . . . . . . . . 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 5945	. . . . . . . . . . . 12 |- ( i e. A |-> ( e ` i ) ) e. _V
35	26, 34	eqeltri 2511	. . . . . . . . . . 11 |- E e. _V
36	35	elixp 7266	. . . . . . . . . 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 2532	. . . . . . . 8 |- ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> E e. P )
40		foelrn 5859	. . . . . . . . . 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 2505	. . . . . . . . . . . . . 14 |- ( a e. S <-> a e. U_ i e. A ( M ` i ) )
44		eliun 4172	. . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . 15 |- F/ i A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) )
47		nfv 1678	. . . . . . . . . . . . . . 15 |- F/ i E = ( f ` a )
48	46, 47	nfan 1865	. . . . . . . . . . . . . 14 |- F/ i ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) )
49		nfv 1678	. . . . . . . . . . . . . 14 |- F/ i -. f = f
50	28	ad2antrl 722	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( E ` i ) = ( e ` i ) )
51		fveq1 5687	. . . . . . . . . . . . . . . . . . . . 21 |- ( E = ( f ` a ) -> ( E ` i ) = ( ( f ` a ) ` i ) )
52	8	fveq1d 5690	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( i e. A -> ( ( D ` i ) ` a ) = ( ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) ` a ) )
53	3	fvmpt2 5778	. . . . . . . . . . . . . . . . . . . . . . . 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 666	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a e. ( M ` i ) -> ( ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) ` a ) = ( ( f ` a ) ` i ) )
55	52, 54	sylan9eq 2493	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( i e. A /\ a e. ( M ` i ) ) -> ( ( D ` i ) ` a ) = ( ( f ` a ) ` i ) )
56	55	eqcomd 2446	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i e. A /\ a e. ( M ` i ) ) -> ( ( f ` a ) ` i ) = ( ( D ` i ) ` a ) )
57	51, 56	sylan9eq 2493	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( E ` i ) = ( ( D ` i ) ` a ) )
58	50, 57	eqtr3d 2475	. . . . . . . . . . . . . . . . . . 19 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( e ` i ) = ( ( D ` i ) ` a ) )
59		fnfvelrn 5837	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( D ` i ) Fn ( M ` i ) /\ a e. ( M ` i ) ) -> ( ( D ` i ) ` a ) e. ran ( D ` i ) )
60	10, 59	sylan 468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. A /\ a e. ( M ` i ) ) -> ( ( D ` i ) ` a ) e. ran ( D ` i ) )
61	60	adantl 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( ( D ` i ) ` a ) e. ran ( D ` i ) )
62	58, 61	eqeltrd 2515	. . . . . . . . . . . . . . . . . 18 |- ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( e ` i ) e. ran ( D ` i ) )
63	62	3adant1 1001	. . . . . . . . . . . . . . . . 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 983	. . . . . . . . . . . . . . . . . 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 1011	. . . . . . . . . . . . . . . . . 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 2774	. . . . . . . . . . . . . . . . . . 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 3476	. . . . . . . . . . . . . . . . . . 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 1184	. . . . . . . . . . . . . . 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 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 2836	. . . . . . . . . . . . 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 2838	. . . . . . . . 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 1693	. . . . 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 1939	. . 3 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> -. E. f f : S -onto-> P )
84	1	0dom 7437	. . . . . . . 8 |- (/) ~<_ ( M ` i )
85		domsdomtr 7442	. . . . . . . 8 |- ( ( (/) ~<_ ( M ` i ) /\ ( M ` i ) ~< ( N ` i ) ) -> (/) ~< ( N ` i ) )
86	84, 85	mpan 665	. . . . . . 7 |- ( ( M ` i ) ~< ( N ` i ) -> (/) ~< ( N ` i ) )
87	19	0sdom 7438	. . . . . . 7 |- ( (/) ~< ( N ` i ) <-> ( N ` i ) =/= (/) )
88	86, 87	sylib 196	. . . . . 6 |- ( ( M ` i ) ~< ( N ` i ) -> ( N ` i ) =/= (/) )
89	88	ralimi 2789	. . . . 5 |- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> A. i e. A ( N ` i ) =/= (/) )
90	38	neeq1i 2616	. . . . . 6 |- ( P =/= (/) <-> X_ i e. A ( N ` i ) =/= (/) )
91	19	rgenw 2781	. . . . . . . . 9 |- A. i e. A ( N ` i ) e. _V
92		ixpexg 7283	. . . . . . . . 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 2511	. . . . . . 7 |- P e. _V
95	94	0sdom 7438	. . . . . 6 |- ( (/) ~< P <-> P =/= (/) )
96	18, 19	ac9 8648	. . . . . 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 6556	. . . . . . 7 |- U_ i e. A ( M ` i ) e. _V
100	42, 99	eqeltri 2511	. . . . . 6 |- S e. _V
101		domtri 8716	. . . . . 6 |- ( ( P e. _V /\ S e. _V ) -> ( P ~<_ S <-> -. S ~< P ) )
102	94, 100, 101	mp2an 667	. . . . 5 |- ( P ~<_ S <-> -. S ~< P )
103	102	biimpri 206	. . . 4 |- ( -. S ~< P -> P ~<_ S )
104		fodomr 7458	. . . 4 |- ( ( (/) ~< P /\ P ~<_ S ) -> E. f f : S -onto-> P )
105	98, 103, 104	syl2an 474	. . 3 |- ( ( A. i e. A ( M ` i ) ~< ( N ` i ) /\ -. S ~< P ) -> E. f f : S -onto-> P )
106	83, 105	mtand 654	. 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 960   = wceq 1364   E.wex 1591   e. wcel 1761   =/= wne 2604   A.wral 2713   E.wrex 2714   _Vcvv 2970   \ cdif 3322   (/)c0 3634   U_ciun 4168   class class class wbr 4289   e. cmpt 4347   ran crn 4837   Fn wfn 5410   -onto->wfo 5413   ` cfv 5415   X_cixp 7259   ~<_ cdom 7304   ~< csdm 7305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-ac2 8628

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-se 4676  df-we 4677  df-ord 4718  df-on 4719  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-isom 5424  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-1st 6576  df-2nd 6577  df-recs 6828  df-er 7097  df-map 7212  df-ixp 7260  df-en 7307  df-dom 7308  df-sdom 7309  df-card 8105  df-acn 8108  df-ac 8282

This theorem is referenced by:  konigth  8729