Metamath Proof Explorer

Theorem konigthlem

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

Ref Expression
Hypotheses konigth.1 ⊢A∈V
konigth.2 ⊢S=⋃i∈AM⁡i
konigth.3 ⊢P=⨉i∈AN⁡i
konigth.4 ⊢D=i∈A⟼a∈M⁡i⟼f⁡a⁡i
konigth.5 ⊢E=i∈A⟼e⁡i
Assertion konigthlem ⊢∀i∈AM⁡i≺N⁡i→S≺P

Proof

Step Hyp Ref Expression
1 konigth.1 ⊢A∈V
2 konigth.2 ⊢S=⋃i∈AM⁡i
3 konigth.3 ⊢P=⨉i∈AN⁡i
4 konigth.4 ⊢D=i∈A⟼a∈M⁡i⟼f⁡a⁡i
5 konigth.5 ⊢E=i∈A⟼e⁡i
6 fvex ⊢M⁡i∈V
7 fvex ⊢f⁡a⁡i∈V
8 eqid ⊢a∈M⁡i⟼f⁡a⁡i=a∈M⁡i⟼f⁡a⁡i
9 7 8 fnmpti ⊢a∈M⁡i⟼f⁡a⁡iFnM⁡i
10 6 mptex ⊢a∈M⁡i⟼f⁡a⁡i∈V
11 4 fvmpt2 ⊢i∈A∧a∈M⁡i⟼f⁡a⁡i∈V→D⁡i=a∈M⁡i⟼f⁡a⁡i
12 10 11 mpan2 ⊢i∈A→D⁡i=a∈M⁡i⟼f⁡a⁡i
13 12 fneq1d ⊢i∈A→D⁡iFnM⁡i↔a∈M⁡i⟼f⁡a⁡iFnM⁡i
14 9 13 mpbiri ⊢i∈A→D⁡iFnM⁡i
15 fnrndomg ⊢M⁡i∈V→D⁡iFnM⁡i→ran⁡D⁡i≼M⁡i
16 6 14 15 mpsyl ⊢i∈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∈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∈A∧M⁡i≺N⁡i→N⁡i∖ran⁡D⁡i≠∅
21 20 ralimiaa ⊢∀i∈AM⁡i≺N⁡i→∀i∈AN⁡i∖ran⁡D⁡i≠∅
22 fvex ⊢N⁡i∈V
23 22 difexi ⊢N⁡i∖ran⁡D⁡i∈V
24 1 23 ac6c5 ⊢∀i∈AN⁡i∖ran⁡D⁡i≠∅→∃e∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i
25 equid ⊢f=f
26 eldifi ⊢e⁡i∈N⁡i∖ran⁡D⁡i→e⁡i∈N⁡i
27 fvex ⊢e⁡i∈V
28 5 fvmpt2 ⊢i∈A∧e⁡i∈V→E⁡i=e⁡i
29 27 28 mpan2 ⊢i∈A→E⁡i=e⁡i
30 29 eleq1d ⊢i∈A→E⁡i∈N⁡i↔e⁡i∈N⁡i
31 26 30 imbitrrid ⊢i∈A→e⁡i∈N⁡i∖ran⁡D⁡i→E⁡i∈N⁡i
32 31 ralimia ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i→∀i∈AE⁡i∈N⁡i
33 27 5 fnmpti ⊢EFnA
34 32 33 jctil ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i→EFnA∧∀i∈AE⁡i∈N⁡i
35 1 mptex ⊢i∈A⟼e⁡i∈V
36 5 35 eqeltri ⊢E∈V
37 36 elixp ⊢E∈⨉i∈AN⁡i↔EFnA∧∀i∈AE⁡i∈N⁡i
38 34 37 sylibr ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i→E∈⨉i∈AN⁡i
39 38 3 eleqtrrdi ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i→E∈P
40 foelrn ⊢f:S⟶ontoP∧E∈P→∃a∈SE=f⁡a
41 40 expcom ⊢E∈P→f:S⟶ontoP→∃a∈SE=f⁡a
42 2 eleq2i ⊢a∈S↔a∈⋃i∈AM⁡i
43 eliun ⊢a∈⋃i∈AM⁡i↔∃i∈Aa∈M⁡i
44 42 43 bitri ⊢a∈S↔∃i∈Aa∈M⁡i
45 nfra1 ⊢Ⅎi∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i
46 nfv ⊢ℲiE=f⁡a
47 45 46 nfan ⊢Ⅎi∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i∧E=f⁡a
48 nfv ⊢Ⅎi¬f=f
49 29 ad2antrl ⊢E=f⁡a∧i∈A∧a∈M⁡i→E⁡i=e⁡i
50 fveq1 ⊢E=f⁡a→E⁡i=f⁡a⁡i
51 12 fveq1d ⊢i∈A→D⁡i⁡a=a∈M⁡i⟼f⁡a⁡i⁡a
52 8 fvmpt2 ⊢a∈M⁡i∧f⁡a⁡i∈V→a∈M⁡i⟼f⁡a⁡i⁡a=f⁡a⁡i
53 7 52 mpan2 ⊢a∈M⁡i→a∈M⁡i⟼f⁡a⁡i⁡a=f⁡a⁡i
54 51 53 sylan9eq ⊢i∈A∧a∈M⁡i→D⁡i⁡a=f⁡a⁡i
55 54 eqcomd ⊢i∈A∧a∈M⁡i→f⁡a⁡i=D⁡i⁡a
56 50 55 sylan9eq ⊢E=f⁡a∧i∈A∧a∈M⁡i→E⁡i=D⁡i⁡a
57 49 56 eqtr3d ⊢E=f⁡a∧i∈A∧a∈M⁡i→e⁡i=D⁡i⁡a
58 fnfvelrn ⊢D⁡iFnM⁡i∧a∈M⁡i→D⁡i⁡a∈ran⁡D⁡i
59 14 58 sylan ⊢i∈A∧a∈M⁡i→D⁡i⁡a∈ran⁡D⁡i
60 59 adantl ⊢E=f⁡a∧i∈A∧a∈M⁡i→D⁡i⁡a∈ran⁡D⁡i
61 57 60 eqeltrd ⊢E=f⁡a∧i∈A∧a∈M⁡i→e⁡i∈ran⁡D⁡i
62 61 3adant1 ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i∧E=f⁡a∧i∈A∧a∈M⁡i→e⁡i∈ran⁡D⁡i
63 simp1 ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i∧E=f⁡a∧i∈A∧a∈M⁡i→∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i
64 simp3l ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i∧E=f⁡a∧i∈A∧a∈M⁡i→i∈A
65 rsp ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i→i∈A→e⁡i∈N⁡i∖ran⁡D⁡i
66 eldifn ⊢e⁡i∈N⁡i∖ran⁡D⁡i→¬e⁡i∈ran⁡D⁡i
67 65 66 syl6 ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i→i∈A→¬e⁡i∈ran⁡D⁡i
68 63 64 67 sylc ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i∧E=f⁡a∧i∈A∧a∈M⁡i→¬e⁡i∈ran⁡D⁡i
69 62 68 pm2.21dd ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i∧E=f⁡a∧i∈A∧a∈M⁡i→¬f=f
70 69 3expia ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i∧E=f⁡a→i∈A∧a∈M⁡i→¬f=f
71 70 expd ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i∧E=f⁡a→i∈A→a∈M⁡i→¬f=f
72 47 48 71 rexlimd ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i∧E=f⁡a→∃i∈Aa∈M⁡i→¬f=f
73 44 72 biimtrid ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i∧E=f⁡a→a∈S→¬f=f
74 73 ex ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i→E=f⁡a→a∈S→¬f=f
75 74 com23 ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i→a∈S→E=f⁡a→¬f=f
76 75 rexlimdv ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i→∃a∈SE=f⁡a→¬f=f
77 41 76 syl9r ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i→E∈P→f:S⟶ontoP→¬f=f
78 39 77 mpd ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i→f:S⟶ontoP→¬f=f
79 25 78 mt2i ⊢∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i→¬f:S⟶ontoP
80 79 exlimiv ⊢∃e∀i∈Ae⁡i∈N⁡i∖ran⁡D⁡i→¬f:S⟶ontoP
81 21 24 80 3syl ⊢∀i∈AM⁡i≺N⁡i→¬f:S⟶ontoP
82 81 nexdv ⊢∀i∈AM⁡i≺N⁡i→¬∃ff:S⟶ontoP
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 ⊢∀i∈AM⁡i≺N⁡i→∀i∈AN⁡i≠∅
89 3 neeq1i ⊢P≠∅↔⨉i∈AN⁡i≠∅
90 22 rgenw ⊢∀i∈AN⁡i∈V
91 ixpexg ⊢∀i∈AN⁡i∈V→⨉i∈AN⁡i∈V
92 90 91 ax-mp ⊢⨉i∈AN⁡i∈V
93 3 92 eqeltri ⊢P∈V
94 93 0sdom ⊢∅≺P↔P≠∅
95 1 22 ac9 ⊢∀i∈AN⁡i≠∅↔⨉i∈AN⁡i≠∅
96 89 94 95 3bitr4i ⊢∅≺P↔∀i∈AN⁡i≠∅
97 88 96 sylibr ⊢∀i∈AM⁡i≺N⁡i→∅≺P
98 1 6 iunex ⊢⋃i∈AM⁡i∈V
99 2 98 eqeltri ⊢S∈V
100 domtri ⊢P∈V∧S∈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→∃ff:S⟶ontoP
104 97 102 103 syl2an ⊢∀i∈AM⁡i≺N⁡i∧¬S≺P→∃ff:S⟶ontoP
105 82 104 mtand ⊢∀i∈AM⁡i≺N⁡i→¬¬S≺P
106 105 notnotrd ⊢∀i∈AM⁡i≺N⁡i→S≺P