Metamath Proof Explorer

Theorem konigthlem

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

Ref Expression
Hypotheses 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 konigthlem 
|- ( A. i e. A ( M ` i ) ~< ( N ` i ) -> S ~< P )

Proof

Step Hyp Ref Expression
1 konigth.1 
 |-  A e. _V
2 konigth.2 
 |-  S = U_ i e. A ( M ` i )
3 konigth.3 
 |-  P = X_ i e. A ( N ` i )
4 konigth.4 
 |-  D = ( i e. A |-> ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) )
5 konigth.5 
 |-  E = ( i e. A |-> ( e ` i ) )
6 fvex 
 |-  ( M ` i ) e. _V
7 fvex 
 |-  ( ( f ` a ) ` i ) e. _V
8 eqid 
 |-  ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) = ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) )
9 7 8 fnmpti 
 |-  ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) Fn ( M ` i )
10 6 mptex 
 |-  ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) e. _V
11 4 fvmpt2 
 |-  ( ( i e. A /\ ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) e. _V ) -> ( D ` i ) = ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) )
12 10 11 mpan2 
 |-  ( i e. A -> ( D ` i ) = ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) )
13 12 fneq1d 
 |-  ( i e. A -> ( ( D ` i ) Fn ( M ` i ) <-> ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) Fn ( M ` i ) ) )
14 9 13 mpbiri 
 |-  ( i e. A -> ( D ` i ) Fn ( M ` i ) )
15 fnrndomg 
 |-  ( ( M ` i ) e. _V -> ( ( D ` i ) Fn ( M ` i ) -> ran ( D ` i ) ~<_ ( M ` i ) ) )
16 6 14 15 mpsyl 
 |-  ( i e. A -> ran ( D ` i ) ~<_ ( M ` i ) )
17 domsdomtr 
 |-  ( ( ran ( D ` i ) ~<_ ( M ` i ) /\ ( M ` i ) ~< ( N ` i ) ) -> ran ( D ` i ) ~< ( N ` i ) )
18 16 17 sylan 
 |-  ( ( i e. A /\ ( M ` i ) ~< ( N ` i ) ) -> ran ( D ` i ) ~< ( N ` i ) )
19 sdomdif 
 |-  ( ran ( D ` i ) ~< ( N ` i ) -> ( ( N ` i ) \ ran ( D ` i ) ) =/= (/) )
20 18 19 syl 
 |-  ( ( i e. A /\ ( M ` i ) ~< ( N ` i ) ) -> ( ( N ` i ) \ ran ( D ` i ) ) =/= (/) )
21 20 ralimiaa 
 |-  ( A. i e. A ( M ` i ) ~< ( N ` i ) -> A. i e. A ( ( N ` i ) \ ran ( D ` i ) ) =/= (/) )
22 fvex 
 |-  ( N ` i ) e. _V
23 22 difexi 
 |-  ( ( N ` i ) \ ran ( D ` i ) ) e. _V
24 1 23 ac6c5 
 |-  ( A. i e. A ( ( N ` i ) \ ran ( D ` i ) ) =/= (/) -> E. e A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) )
25 equid 
 |-  f = f
26 eldifi 
 |-  ( ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( e ` i ) e. ( N ` i ) )
27 fvex 
 |-  ( e ` i ) e. _V
28 5 fvmpt2 
 |-  ( ( i e. A /\ ( e ` i ) e. _V ) -> ( E ` i ) = ( e ` i ) )
29 27 28 mpan2 
 |-  ( i e. A -> ( E ` i ) = ( e ` i ) )
30 29 eleq1d 
 |-  ( i e. A -> ( ( E ` i ) e. ( N ` i ) <-> ( e ` i ) e. ( N ` i ) ) )
31 26 30 syl5ibr 
 |-  ( i e. A -> ( ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( E ` i ) e. ( N ` i ) ) )
32 31 ralimia 
 |-  ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> A. i e. A ( E ` i ) e. ( N ` i ) )
33 27 5 fnmpti 
 |-  E Fn A
34 32 33 jctil 
 |-  ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( E Fn A /\ A. i e. A ( E ` i ) e. ( N ` i ) ) )
35 1 mptex 
 |-  ( i e. A |-> ( e ` i ) ) e. _V
36 5 35 eqeltri 
 |-  E e. _V
37 36 elixp 
 |-  ( E e. X_ i e. A ( N ` i ) <-> ( E Fn A /\ A. i e. A ( E ` i ) e. ( N ` i ) ) )
38 34 37 sylibr 
 |-  ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> E e. X_ i e. A ( N ` i ) )
39 38 3 eleqtrrdi 
 |-  ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> E e. P )
40 foelrn 
 |-  ( ( f : S -onto-> P /\ E e. P ) -> E. a e. S E = ( f ` a ) )
41 40 expcom 
 |-  ( E e. P -> ( f : S -onto-> P -> E. a e. S E = ( f ` a ) ) )
42 2 eleq2i 
 |-  ( a e. S <-> a e. U_ i e. A ( M ` i ) )
43 eliun 
 |-  ( a e. U_ i e. A ( M ` i ) <-> E. i e. A a e. ( M ` i ) )
44 42 43 bitri 
 |-  ( a e. S <-> E. i e. A a e. ( M ` i ) )
45 nfra1 
 |-  F/ i A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) )
46 nfv 
 |-  F/ i E = ( f ` a )
47 45 46 nfan 
 |-  F/ i ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) )
48 nfv 
 |-  F/ i -. f = f
49 29 ad2antrl 
 |-  ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( E ` i ) = ( e ` i ) )
50 fveq1 
 |-  ( E = ( f ` a ) -> ( E ` i ) = ( ( f ` a ) ` i ) )
51 12 fveq1d 
 |-  ( i e. A -> ( ( D ` i ) ` a ) = ( ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) ` a ) )
52 8 fvmpt2 
 |-  ( ( a e. ( M ` i ) /\ ( ( f ` a ) ` i ) e. _V ) -> ( ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) ` a ) = ( ( f ` a ) ` i ) )
53 7 52 mpan2 
 |-  ( a e. ( M ` i ) -> ( ( a e. ( M ` i ) |-> ( ( f ` a ) ` i ) ) ` a ) = ( ( f ` a ) ` i ) )
54 51 53 sylan9eq 
 |-  ( ( i e. A /\ a e. ( M ` i ) ) -> ( ( D ` i ) ` a ) = ( ( f ` a ) ` i ) )
55 54 eqcomd 
 |-  ( ( i e. A /\ a e. ( M ` i ) ) -> ( ( f ` a ) ` i ) = ( ( D ` i ) ` a ) )
56 50 55 sylan9eq 
 |-  ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( E ` i ) = ( ( D ` i ) ` a ) )
57 49 56 eqtr3d 
 |-  ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( e ` i ) = ( ( D ` i ) ` a ) )
58 fnfvelrn 
 |-  ( ( ( D ` i ) Fn ( M ` i ) /\ a e. ( M ` i ) ) -> ( ( D ` i ) ` a ) e. ran ( D ` i ) )
59 14 58 sylan 
 |-  ( ( i e. A /\ a e. ( M ` i ) ) -> ( ( D ` i ) ` a ) e. ran ( D ` i ) )
60 59 adantl 
 |-  ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( ( D ` i ) ` a ) e. ran ( D ` i ) )
61 57 60 eqeltrd 
 |-  ( ( E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> ( e ` i ) e. ran ( D ` i ) )
62 61 3adant1 
 |-  ( ( 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 ) )
63 simp1 
 |-  ( ( 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 ) ) )
64 simp3l 
 |-  ( ( 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 )
65 rsp 
 |-  ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( i e. A -> ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) ) )
66 eldifn 
 |-  ( ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> -. ( e ` i ) e. ran ( D ` i ) )
67 65 66 syl6 
 |-  ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( i e. A -> -. ( e ` i ) e. ran ( D ` i ) ) )
68 63 64 67 sylc 
 |-  ( ( 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 ) )
69 62 68 pm2.21dd 
 |-  ( ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) /\ ( i e. A /\ a e. ( M ` i ) ) ) -> -. f = f )
70 69 3expia 
 |-  ( ( 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 expd 
 |-  ( ( 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 47 48 71 rexlimd 
 |-  ( ( 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 ) )
73 44 72 syl5bi 
 |-  ( ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) /\ E = ( f ` a ) ) -> ( a e. S -> -. f = f ) )
74 73 ex 
 |-  ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( E = ( f ` a ) -> ( a e. S -> -. f = f ) ) )
75 74 com23 
 |-  ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( a e. S -> ( E = ( f ` a ) -> -. f = f ) ) )
76 75 rexlimdv 
 |-  ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( E. a e. S E = ( f ` a ) -> -. f = f ) )
77 41 76 syl9r 
 |-  ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( E e. P -> ( f : S -onto-> P -> -. f = f ) ) )
78 39 77 mpd 
 |-  ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> ( f : S -onto-> P -> -. f = f ) )
79 25 78 mt2i 
 |-  ( A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> -. f : S -onto-> P )
80 79 exlimiv 
 |-  ( E. e A. i e. A ( e ` i ) e. ( ( N ` i ) \ ran ( D ` i ) ) -> -. f : S -onto-> P )
81 21 24 80 3syl 
 |-  ( A. i e. A ( M ` i ) ~< ( N ` i ) -> -. f : S -onto-> P )
82 81 nexdv 
 |-  ( A. i e. A ( M ` i ) ~< ( N ` i ) -> -. E. f f : S -onto-> P )
83 6 0dom 
 |-  (/) ~<_ ( M ` i )
84 domsdomtr 
 |-  ( ( (/) ~<_ ( M ` i ) /\ ( M ` i ) ~< ( N ` i ) ) -> (/) ~< ( N ` i ) )
85 83 84 mpan 
 |-  ( ( M ` i ) ~< ( N ` i ) -> (/) ~< ( N ` i ) )
86 22 0sdom 
 |-  ( (/) ~< ( N ` i ) <-> ( N ` i ) =/= (/) )
87 85 86 sylib 
 |-  ( ( M ` i ) ~< ( N ` i ) -> ( N ` i ) =/= (/) )
88 87 ralimi 
 |-  ( A. i e. A ( M ` i ) ~< ( N ` i ) -> A. i e. A ( N ` i ) =/= (/) )
89 3 neeq1i 
 |-  ( P =/= (/) <-> X_ i e. A ( N ` i ) =/= (/) )
90 22 rgenw 
 |-  A. i e. A ( N ` i ) e. _V
91 ixpexg 
 |-  ( A. i e. A ( N ` i ) e. _V -> X_ i e. A ( N ` i ) e. _V )
92 90 91 ax-mp 
 |-  X_ i e. A ( N ` i ) e. _V
93 3 92 eqeltri 
 |-  P e. _V
94 93 0sdom 
 |-  ( (/) ~< P <-> P =/= (/) )
95 1 22 ac9 
 |-  ( A. i e. A ( N ` i ) =/= (/) <-> X_ i e. A ( N ` i ) =/= (/) )
96 89 94 95 3bitr4i 
 |-  ( (/) ~< P <-> A. i e. A ( N ` i ) =/= (/) )
97 88 96 sylibr 
 |-  ( A. i e. A ( M ` i ) ~< ( N ` i ) -> (/) ~< P )
98 1 6 iunex 
 |-  U_ i e. A ( M ` i ) e. _V
99 2 98 eqeltri 
 |-  S e. _V
100 domtri 
 |-  ( ( P e. _V /\ S e. _V ) -> ( P ~<_ S <-> -. S ~< P ) )
101 93 99 100 mp2an 
 |-  ( P ~<_ S <-> -. S ~< P )
102 101 biimpri 
 |-  ( -. S ~< P -> P ~<_ S )
103 fodomr 
 |-  ( ( (/) ~< P /\ P ~<_ S ) -> E. f f : S -onto-> P )
104 97 102 103 syl2an 
 |-  ( ( A. i e. A ( M ` i ) ~< ( N ` i ) /\ -. S ~< P ) -> E. f f : S -onto-> P )
105 82 104 mtand 
 |-  ( A. i e. A ( M ` i ) ~< ( N ` i ) -> -. -. S ~< P )
106 105 notnotrd 
 |-  ( A. i e. A ( M ` i ) ~< ( N ` i ) -> S ~< P )