Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fnwe2lem2 Unicode version

Theorem fnwe2lem2 27016
 Description: Lemma for fnwe2 27018. An element which is in a minimal fiber and minimal within its fiber is minimal globally; thus is well-founded. (Contributed by Stefan O'Rear, 19-Jan-2015.)
Hypotheses
Ref Expression
fnwe2.su
fnwe2.t
fnwe2.s
fnwe2.f
fnwe2.r
fnwe2lem2.a
fnwe2lem2.n0
Assertion
Ref Expression
fnwe2lem2
Distinct variable groups:   ,,,,,   ,,,,,   ,,,,,   ,,,,   ,,,,,,   ,,,,,,   ,,,   ,,,   ,
Allowed substitution hints:   ()   (,,)   ()   ()   (,,)   ()

Proof of Theorem fnwe2lem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fnwe2.f . . . 4
2 ffun 5552 . . . 4
3 vex 2919 . . . . 5
43funimaex 5490 . . . 4
51, 2, 43syl 19 . . 3
6 fnwe2.r . . . 4
7 wefr 4532 . . . 4
86, 7syl 16 . . 3
9 imassrn 5175 . . . 4
10 frn 5556 . . . . 5
111, 10syl 16 . . . 4
129, 11syl5ss 3319 . . 3
13 incom 3493 . . . . . 6
14 fnwe2lem2.a . . . . . . . 8
15 fdm 5554 . . . . . . . . 9
161, 15syl 16 . . . . . . . 8
1714, 16sseqtr4d 3345 . . . . . . 7
18 df-ss 3294 . . . . . . 7
1917, 18sylib 189 . . . . . 6
2013, 19syl5eq 2448 . . . . 5
21 fnwe2lem2.n0 . . . . 5
2220, 21eqnetrd 2585 . . . 4
23 imadisj 5182 . . . . 5
2423necon3bii 2599 . . . 4
2522, 24sylibr 204 . . 3
26 fri 4504 . . 3
275, 8, 12, 25, 26syl22anc 1185 . 2
28 df-ima 4850 . . . . . 6
2928rexeqi 2869 . . . . 5
30 ffn 5550 . . . . . . . 8
311, 30syl 16 . . . . . . 7
32 fnssres 5517 . . . . . . 7
3331, 14, 32syl2anc 643 . . . . . 6
34 breq2 4176 . . . . . . . . 9
3534notbid 286 . . . . . . . 8
3635ralbidv 2686 . . . . . . 7
3736rexrn 5831 . . . . . 6
3833, 37syl 16 . . . . 5
3929, 38syl5bb 249 . . . 4
4028raleqi 2868 . . . . . . . 8
41 breq1 4175 . . . . . . . . . . 11
4241notbid 286 . . . . . . . . . 10
4342ralrn 5832 . . . . . . . . 9
4433, 43syl 16 . . . . . . . 8
4540, 44syl5bb 249 . . . . . . 7
4645adantr 452 . . . . . 6
47 resabs1 5134 . . . . . . . . . . . . 13
4814, 47syl 16 . . . . . . . . . . . 12
4948ad2antrr 707 . . . . . . . . . . 11
5049fveq1d 5689 . . . . . . . . . 10
51 fvres 5704 . . . . . . . . . . 11
5251adantl 453 . . . . . . . . . 10
5350, 52eqtrd 2436 . . . . . . . . 9
5449fveq1d 5689 . . . . . . . . . 10
55 fvres 5704 . . . . . . . . . . 11
5655ad2antlr 708 . . . . . . . . . 10
5754, 56eqtrd 2436 . . . . . . . . 9
5853, 57breq12d 4185 . . . . . . . 8
5958notbid 286 . . . . . . 7
6059ralbidva 2682 . . . . . 6
6146, 60bitrd 245 . . . . 5
6261rexbidva 2683 . . . 4
6339, 62bitrd 245 . . 3
643inex1 4304 . . . . . . 7
6564a1i 11 . . . . . 6
6614sselda 3308 . . . . . . . 8
67 fnwe2.su . . . . . . . . . 10
68 fnwe2.t . . . . . . . . . 10
69 fnwe2.s . . . . . . . . . 10
7067, 68, 69fnwe2lem1 27015 . . . . . . . . 9
71 wefr 4532 . . . . . . . . 9
7270, 71syl 16 . . . . . . . 8
7366, 72syldan 457 . . . . . . 7
7473adantrr 698 . . . . . 6
75 inss2 3522 . . . . . . 7
7675a1i 11 . . . . . 6
77 simprl 733 . . . . . . . 8
7866adantrr 698 . . . . . . . . 9
79 eqidd 2405 . . . . . . . . 9
80 fveq2 5687 . . . . . . . . . . 11
8180eqeq1d 2412 . . . . . . . . . 10
8281elrab 3052 . . . . . . . . 9
8378, 79, 82sylanbrc 646 . . . . . . . 8
84 elin 3490 . . . . . . . 8
8577, 83, 84sylanbrc 646 . . . . . . 7
86 ne0i 3594 . . . . . . 7
8785, 86syl 16 . . . . . 6
88 fri 4504 . . . . . 6
8965, 74, 76, 87, 88syl22anc 1185 . . . . 5
90 elin 3490 . . . . . . . 8
91 fveq2 5687 . . . . . . . . . . 11
9291eqeq1d 2412 . . . . . . . . . 10
9392elrab 3052 . . . . . . . . 9
9493anbi2i 676 . . . . . . . 8
9590, 94bitri 241 . . . . . . 7
96 elin 3490 . . . . . . . . . . . . 13
97 fveq2 5687 . . . . . . . . . . . . . . . 16
9897eqeq1d 2412 . . . . . . . . . . . . . . 15
9998elrab 3052 . . . . . . . . . . . . . 14
10099anbi2i 676 . . . . . . . . . . . . 13
10196, 100bitri 241 . . . . . . . . . . . 12
102101imbi1i 316 . . . . . . . . . . 11
103 impexp 434 . . . . . . . . . . 11
104102, 103bitri 241 . . . . . . . . . 10
105104ralbii2 2694 . . . . . . . . 9
106 simplrl 737 . . . . . . . . . . 11
107 simpr 448 . . . . . . . . . . . . . . . 16
108 simplrr 738 . . . . . . . . . . . . . . . . 17
109108ad2antrr 707 . . . . . . . . . . . . . . . 16
110 fveq2 5687 . . . . . . . . . . . . . . . . . . 19
111110breq1d 4182 . . . . . . . . . . . . . . . . . 18
112111notbid 286 . . . . . . . . . . . . . . . . 17
113112rspcva 3010 . . . . . . . . . . . . . . . 16
114107, 109, 113syl2anc 643 . . . . . . . . . . . . . . 15
115 simprrr 742 . . . . . . . . . . . . . . . . 17
116115ad2antrr 707 . . . . . . . . . . . . . . . 16
117116breq2d 4184 . . . . . . . . . . . . . . 15
118114, 117mtbird 293 . . . . . . . . . . . . . 14
11914ad3antrrr 711 . . . . . . . . . . . . . . . . . . . 20
120119sselda 3308 . . . . . . . . . . . . . . . . . . 19
121120adantrr 698 . . . . . . . . . . . . . . . . . 18
122 simprr 734 . . . . . . . . . . . . . . . . . . 19
123115ad2antrr 707 . . . . . . . . . . . . . . . . . . 19
124122, 123eqtrd 2436 . . . . . . . . . . . . . . . . . 18
125 simprl 733 . . . . . . . . . . . . . . . . . . 19
126 simplr 732 . . . . . . . . . . . . . . . . . . 19
127 eleq1 2464 . . . . . . . . . . . . . . . . . . . . . 22
128 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . 23
129128eqeq1d 2412 . . . . . . . . . . . . . . . . . . . . . 22
130127, 129anbi12d 692 . . . . . . . . . . . . . . . . . . . . 21
131 breq1 4175 . . . . . . . . . . . . . . . . . . . . . 22
132131notbid 286 . . . . . . . . . . . . . . . . . . . . 21
133130, 132imbi12d 312 . . . . . . . . . . . . . . . . . . . 20
134133rspcva 3010 . . . . . . . . . . . . . . . . . . 19
135125, 126, 134syl2anc 643 . . . . . . . . . . . . . . . . . 18
136121, 124, 135mp2and 661 . . . . . . . . . . . . . . . . 17
137122, 123eqtr2d 2437 . . . . . . . . . . . . . . . . . . 19
138137csbeq1d 3217 . . . . . . . . . . . . . . . . . 18
139138breqd 4183 . . . . . . . . . . . . . . . . 17
140136, 139mtbid 292 . . . . . . . . . . . . . . . 16
141140expr 599 . . . . . . . . . . . . . . 15
142 imnan 412 . . . . . . . . . . . . . . 15
143141, 142sylib 189 . . . . . . . . . . . . . 14
144 ioran 477 . . . . . . . . . . . . . 14
145118, 143, 144sylanbrc 646 . . . . . . . . . . . . 13
14667, 68fnwe2val 27014 . . . . . . . . . . . . 13
147145, 146sylnibr 297 . . . . . . . . . . . 12
148147ralrimiva 2749 . . . . . . . . . . 11
149 breq2 4176 . . . . . . . . . . . . . 14
150149notbid 286 . . . . . . . . . . . . 13
151150ralbidv 2686 . . . . . . . . . . . 12
152151rspcev 3012 . . . . . . . . . . 11
153106, 148, 152syl2anc 643 . . . . . . . . . 10
154153ex 424 . . . . . . . . 9
155105, 154syl5bi 209 . . . . . . . 8
156155ex 424 . . . . . . 7
15795, 156syl5bi 209 . . . . . 6
158157rexlimdv 2789 . . . . 5
15989, 158mpd 15 . . . 4
160159rexlimdvaa 2791 . . 3
16163, 160sylbid 207 . 2
16227, 161mpd 15 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   wceq 1649   wcel 1721   wne 2567  wral 2666  wrex 2667  crab 2670  cvv 2916  csb 3211   cin 3279   wss 3280  c0 3588   class class class wbr 4172  copab 4225   wfr 4498   wwe 4500   cdm 4837   crn 4838   cres 4839  cima 4840   wfun 5407   wfn 5408  wf 5409  cfv 5413 This theorem is referenced by:  fnwe2  27018 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pr 4363 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421
 Copyright terms: Public domain W3C validator