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 )