Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tz7.48-2 Structured version   Unicode version

Theorem tz7.48-2 7164
 Description: Proposition 7.48(2) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.) (Revised by David Abernethy, 5-May-2013.)
Hypothesis
Ref Expression
tz7.48.1
Assertion
Ref Expression
tz7.48-2
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem tz7.48-2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ssid 3483 . . 3
2 onelon 5464 . . . . . . . . 9
32ancoms 454 . . . . . . . 8
4 tz7.48.1 . . . . . . . . . . 11
5 fndm 5690 . . . . . . . . . . 11
64, 5ax-mp 5 . . . . . . . . . 10
76eleq2i 2500 . . . . . . . . 9
8 fnfun 5688 . . . . . . . . . . . . 13
94, 8ax-mp 5 . . . . . . . . . . . 12
10 funfvima 6152 . . . . . . . . . . . 12
119, 10mpan 674 . . . . . . . . . . 11
1211impcom 431 . . . . . . . . . 10
13 eleq1a 2505 . . . . . . . . . . 11
14 eldifn 3588 . . . . . . . . . . 11
1513, 14nsyli 146 . . . . . . . . . 10
1612, 15syl 17 . . . . . . . . 9
177, 16sylan2br 478 . . . . . . . 8
183, 17syldan 472 . . . . . . 7
1918expimpd 606 . . . . . 6
2019com12 32 . . . . 5
2120ralrimiv 2837 . . . 4
2221ralimiaa 2817 . . 3
234tz7.48lem 7163 . . 3
241, 22, 23sylancr 667 . 2
25 fnrel 5689 . . . . . 6
264, 25ax-mp 5 . . . . 5
276eqimssi 3518 . . . . 5
28 relssres 5158 . . . . 5
2926, 27, 28mp2an 676 . . . 4
3029cnveqi 5025 . . 3
3130funeqi 5618 . 2
3224, 31sylib 199 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 370   wceq 1437   wcel 1868  wral 2775   cdif 3433   wss 3436  ccnv 4849   cdm 4850   cres 4852  cima 4853   wrel 4855  con0 5439   wfun 5592   wfn 5593  cfv 5598 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-tr 4516  df-eprel 4761  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-ord 5442  df-on 5443  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fv 5606 This theorem is referenced by:  tz7.48-3  7166
 Copyright terms: Public domain W3C validator