MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tz7.49 Unicode version

Theorem tz7.49 7129
Description: Proposition 7.49 of [TakeutiZaring] p. 51. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 10-Jan-2013.)
Hypotheses
Ref Expression
tz7.49.1
tz7.49.2
Assertion
Ref Expression
tz7.49
Distinct variable groups:   , ,   , ,   ,

Proof of Theorem tz7.49
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-ne 2654 . . . . . . . . 9
21ralbii 2888 . . . . . . . 8
3 tz7.49.2 . . . . . . . . 9
4 ralim 2846 . . . . . . . . 9
53, 4sylbi 195 . . . . . . . 8
62, 5syl5bir 218 . . . . . . 7
7 tz7.49.1 . . . . . . . . 9
87tz7.48-3 7128 . . . . . . . 8
9 elex 3118 . . . . . . . 8
108, 9nsyl3 119 . . . . . . 7
116, 10nsyli 141 . . . . . 6
12 dfrex2 2908 . . . . . 6
1311, 12syl6ibr 227 . . . . 5
14 imaeq2 5338 . . . . . . . 8
1514difeq2d 3621 . . . . . . 7
1615eqeq1d 2459 . . . . . 6
1716onminex 6642 . . . . 5
1813, 17syl6 33 . . . 4
19 df-ne 2654 . . . . . . 7
2019ralbii 2888 . . . . . 6
2120anbi2i 694 . . . . 5
2221rexbii 2959 . . . 4
2318, 22syl6ibr 227 . . 3
24 nfra1 2838 . . . . 5
253, 24nfxfr 1645 . . . 4
26 simpllr 760 . . . . . . . . 9
27 fnfun 5683 . . . . . . . . . . . . . . . . 17
287, 27ax-mp 5 . . . . . . . . . . . . . . . 16
29 fvelima 5925 . . . . . . . . . . . . . . . 16
3028, 29mpan 670 . . . . . . . . . . . . . . 15
31 nfv 1707 . . . . . . . . . . . . . . . . 17
32 nfra1 2838 . . . . . . . . . . . . . . . . 17
3331, 32nfan 1928 . . . . . . . . . . . . . . . 16
34 nfv 1707 . . . . . . . . . . . . . . . 16
35 rsp 2823 . . . . . . . . . . . . . . . . . . . . . . 23
3635adantld 467 . . . . . . . . . . . . . . . . . . . . . 22
37 onelon 4908 . . . . . . . . . . . . . . . . . . . . . . 23
3815neeq1d 2734 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
39 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
4039, 15eleq12d 2539 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4138, 40imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4241rspcv 3206 . . . . . . . . . . . . . . . . . . . . . . . . 25
433, 42syl5bi 217 . . . . . . . . . . . . . . . . . . . . . . . 24
4443com23 78 . . . . . . . . . . . . . . . . . . . . . . 23
4537, 44syl 16 . . . . . . . . . . . . . . . . . . . . . 22
4636, 45sylcom 29 . . . . . . . . . . . . . . . . . . . . 21
4746com3r 79 . . . . . . . . . . . . . . . . . . . 20
4847imp 429 . . . . . . . . . . . . . . . . . . 19
4948expcomd 438 . . . . . . . . . . . . . . . . . 18
50 eldifi 3625 . . . . . . . . . . . . . . . . . . 19
51 eleq1 2529 . . . . . . . . . . . . . . . . . . 19
5250, 51syl5ibcom 220 . . . . . . . . . . . . . . . . . 18
5349, 52syl8 70 . . . . . . . . . . . . . . . . 17
5453com34 83 . . . . . . . . . . . . . . . 16
5533, 34, 54rexlimd 2941 . . . . . . . . . . . . . . 15
5630, 55syl5 32 . . . . . . . . . . . . . 14
5756com23 78 . . . . . . . . . . . . 13
5857imp 429 . . . . . . . . . . . 12
5958ssrdv 3509 . . . . . . . . . . 11
60 ssdif0 3885 . . . . . . . . . . . 12
6160biimpri 206 . . . . . . . . . . 11
6259, 61anim12i 566 . . . . . . . . . 10
63 eqss 3518 . . . . . . . . . 10
6462, 63sylibr 212 . . . . . . . . 9
65 onss 6626 . . . . . . . . . . . . 13
6632, 31nfan 1928 . . . . . . . . . . . . . . . . 17
67 nfv 1707 . . . . . . . . . . . . . . . . 17
6866, 67nfan 1928 . . . . . . . . . . . . . . . 16
69 nfv 1707 . . . . . . . . . . . . . . . . . 18
70 ssel 3497 . . . . . . . . . . . . . . . . . . . . . 22
71 onss 6626 . . . . . . . . . . . . . . . . . . . . . . . 24
72 fndm 5685 . . . . . . . . . . . . . . . . . . . . . . . . 25
737, 72ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24
7471, 73syl6sseqr 3550 . . . . . . . . . . . . . . . . . . . . . . 23
75 funfvima2 6148 . . . . . . . . . . . . . . . . . . . . . . 23
7628, 74, 75sylancr 663 . . . . . . . . . . . . . . . . . . . . . 22
7770, 76syl6 33 . . . . . . . . . . . . . . . . . . . . 21
7835com12 31 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7978a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
8070, 79, 44syl10 73 . . . . . . . . . . . . . . . . . . . . . . . 24
8180imp4a 589 . . . . . . . . . . . . . . . . . . . . . . 23
82 eldifn 3626 . . . . . . . . . . . . . . . . . . . . . . . 24
83 eleq1a 2540 . . . . . . . . . . . . . . . . . . . . . . . . 25
8483con3d 133 . . . . . . . . . . . . . . . . . . . . . . . 24
8582, 84syl5com 30 . . . . . . . . . . . . . . . . . . . . . . 23
8681, 85syl8 70 . . . . . . . . . . . . . . . . . . . . . 22
8786com34 83 . . . . . . . . . . . . . . . . . . . . 21
8877, 87syldd 66 . . . . . . . . . . . . . . . . . . . 20
8988com4r 86 . . . . . . . . . . . . . . . . . . 19
9089imp31 432 . . . . . . . . . . . . . . . . . 18
9169, 90ralrimi 2857 . . . . . . . . . . . . . . . . 17
9291ex 434 . . . . . . . . . . . . . . . 16
9368, 92ralrimi 2857 . . . . . . . . . . . . . . 15
9493ex 434 . . . . . . . . . . . . . 14
9594ancld 553 . . . . . . . . . . . . 13
967tz7.48lem 7125 . . . . . . . . . . . . 13
9765, 95, 96syl56 34 . . . . . . . . . . . 12
9897ancoms 453 . . . . . . . . . . 11
9998imp 429 . . . . . . . . . 10
10099adantr 465 . . . . . . . . 9
10126, 64, 1003jca 1176 . . . . . . . 8
102101exp41 610 . . . . . . 7
103102com23 78 . . . . . 6
104103com34 83 . . . . 5
105104imp4a 589 . . . 4
10625, 105reximdai 2926 . . 3
10723, 106syld 44 . 2
108107impcom 430 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  /\w3a 973  =wceq 1395  e.wcel 1818  =/=wne 2652  A.wral 2807  E.wrex 2808   cvv 3109  \cdif 3472  C_wss 3475   c0 3784   con0 4883  `'ccnv 5003  domcdm 5004  |`cres 5006  "cima 5007  Funwfun 5587  Fnwfn 5588  `cfv 5593
This theorem is referenced by:  tz7.49c  7130
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-int 4287  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601
  Copyright terms: Public domain W3C validator