Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fompt Structured version   Visualization version   Unicode version

Theorem fompt 37461
Description: Express being onto for a mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypothesis
Ref Expression
fompt.1  |-  F  =  ( x  e.  A  |->  C )
Assertion
Ref Expression
fompt  |-  ( F : A -onto-> B  <->  ( A. x  e.  A  C  e.  B  /\  A. y  e.  B  E. x  e.  A  y  =  C ) )
Distinct variable groups:    x, A, y    x, B, y    y, C    y, F
Allowed substitution hints:    C( x)    F( x)

Proof of Theorem fompt
StepHypRef Expression
1 fompt.1 . . . . . . 7  |-  F  =  ( x  e.  A  |->  C )
2 nfmpt1 4491 . . . . . . 7  |-  F/_ x
( x  e.  A  |->  C )
31, 2nfcxfr 2589 . . . . . 6  |-  F/_ x F
43dffo3f 37444 . . . . 5  |-  ( F : A -onto-> B  <->  ( F : A --> B  /\  A. y  e.  B  E. x  e.  A  y  =  ( F `  x ) ) )
54simplbi 462 . . . 4  |-  ( F : A -onto-> B  ->  F : A --> B )
61fmpt 6041 . . . . . 6  |-  ( A. x  e.  A  C  e.  B  <->  F : A --> B )
76bicomi 206 . . . . 5  |-  ( F : A --> B  <->  A. x  e.  A  C  e.  B )
87biimpi 198 . . . 4  |-  ( F : A --> B  ->  A. x  e.  A  C  e.  B )
95, 8syl 17 . . 3  |-  ( F : A -onto-> B  ->  A. x  e.  A  C  e.  B )
103foelrnf 37455 . . . . 5  |-  ( ( F : A -onto-> B  /\  y  e.  B
)  ->  E. x  e.  A  y  =  ( F `  x ) )
11 nfcv 2591 . . . . . . . 8  |-  F/_ x A
12 nfcv 2591 . . . . . . . 8  |-  F/_ x B
133, 11, 12nffo 5790 . . . . . . 7  |-  F/ x  F : A -onto-> B
14 simpr 463 . . . . . . . . . 10  |-  ( ( ( F : A -onto-> B  /\  x  e.  A
)  /\  y  =  ( F `  x ) )  ->  y  =  ( F `  x ) )
15 simpr 463 . . . . . . . . . . . 12  |-  ( ( F : A -onto-> B  /\  x  e.  A
)  ->  x  e.  A )
169r19.21bi 2756 . . . . . . . . . . . 12  |-  ( ( F : A -onto-> B  /\  x  e.  A
)  ->  C  e.  B )
171fvmpt2 5955 . . . . . . . . . . . 12  |-  ( ( x  e.  A  /\  C  e.  B )  ->  ( F `  x
)  =  C )
1815, 16, 17syl2anc 666 . . . . . . . . . . 11  |-  ( ( F : A -onto-> B  /\  x  e.  A
)  ->  ( F `  x )  =  C )
1918adantr 467 . . . . . . . . . 10  |-  ( ( ( F : A -onto-> B  /\  x  e.  A
)  /\  y  =  ( F `  x ) )  ->  ( F `  x )  =  C )
2014, 19eqtrd 2484 . . . . . . . . 9  |-  ( ( ( F : A -onto-> B  /\  x  e.  A
)  /\  y  =  ( F `  x ) )  ->  y  =  C )
2120ex 436 . . . . . . . 8  |-  ( ( F : A -onto-> B  /\  x  e.  A
)  ->  ( y  =  ( F `  x )  ->  y  =  C ) )
2221ex 436 . . . . . . 7  |-  ( F : A -onto-> B  -> 
( x  e.  A  ->  ( y  =  ( F `  x )  ->  y  =  C ) ) )
2313, 22reximdai 2855 . . . . . 6  |-  ( F : A -onto-> B  -> 
( E. x  e.  A  y  =  ( F `  x )  ->  E. x  e.  A  y  =  C )
)
2423adantr 467 . . . . 5  |-  ( ( F : A -onto-> B  /\  y  e.  B
)  ->  ( E. x  e.  A  y  =  ( F `  x )  ->  E. x  e.  A  y  =  C ) )
2510, 24mpd 15 . . . 4  |-  ( ( F : A -onto-> B  /\  y  e.  B
)  ->  E. x  e.  A  y  =  C )
2625ralrimiva 2801 . . 3  |-  ( F : A -onto-> B  ->  A. y  e.  B  E. x  e.  A  y  =  C )
279, 26jca 535 . 2  |-  ( F : A -onto-> B  -> 
( A. x  e.  A  C  e.  B  /\  A. y  e.  B  E. x  e.  A  y  =  C )
)
286biimpi 198 . . . . 5  |-  ( A. x  e.  A  C  e.  B  ->  F : A
--> B )
2928adantr 467 . . . 4  |-  ( ( A. x  e.  A  C  e.  B  /\  A. y  e.  B  E. x  e.  A  y  =  C )  ->  F : A --> B )
30 nfv 1760 . . . . . 6  |-  F/ y A. x  e.  A  C  e.  B
31 nfra1 2768 . . . . . 6  |-  F/ y A. y  e.  B  E. x  e.  A  y  =  C
3230, 31nfan 2010 . . . . 5  |-  F/ y ( A. x  e.  A  C  e.  B  /\  A. y  e.  B  E. x  e.  A  y  =  C )
33 simpll 759 . . . . . . 7  |-  ( ( ( A. x  e.  A  C  e.  B  /\  A. y  e.  B  E. x  e.  A  y  =  C )  /\  y  e.  B
)  ->  A. x  e.  A  C  e.  B )
34 rspa 2754 . . . . . . . 8  |-  ( ( A. y  e.  B  E. x  e.  A  y  =  C  /\  y  e.  B )  ->  E. x  e.  A  y  =  C )
3534adantll 719 . . . . . . 7  |-  ( ( ( A. x  e.  A  C  e.  B  /\  A. y  e.  B  E. x  e.  A  y  =  C )  /\  y  e.  B
)  ->  E. x  e.  A  y  =  C )
36 nfra1 2768 . . . . . . . . 9  |-  F/ x A. x  e.  A  C  e.  B
37 simp3 1009 . . . . . . . . . . 11  |-  ( ( A. x  e.  A  C  e.  B  /\  x  e.  A  /\  y  =  C )  ->  y  =  C )
38 simpr 463 . . . . . . . . . . . . . 14  |-  ( ( A. x  e.  A  C  e.  B  /\  x  e.  A )  ->  x  e.  A )
39 rspa 2754 . . . . . . . . . . . . . 14  |-  ( ( A. x  e.  A  C  e.  B  /\  x  e.  A )  ->  C  e.  B )
4038, 39, 17syl2anc 666 . . . . . . . . . . . . 13  |-  ( ( A. x  e.  A  C  e.  B  /\  x  e.  A )  ->  ( F `  x
)  =  C )
4140eqcomd 2456 . . . . . . . . . . . 12  |-  ( ( A. x  e.  A  C  e.  B  /\  x  e.  A )  ->  C  =  ( F `
 x ) )
42413adant3 1027 . . . . . . . . . . 11  |-  ( ( A. x  e.  A  C  e.  B  /\  x  e.  A  /\  y  =  C )  ->  C  =  ( F `
 x ) )
4337, 42eqtrd 2484 . . . . . . . . . 10  |-  ( ( A. x  e.  A  C  e.  B  /\  x  e.  A  /\  y  =  C )  ->  y  =  ( F `
 x ) )
44433exp 1206 . . . . . . . . 9  |-  ( A. x  e.  A  C  e.  B  ->  ( x  e.  A  ->  (
y  =  C  -> 
y  =  ( F `
 x ) ) ) )
4536, 44reximdai 2855 . . . . . . . 8  |-  ( A. x  e.  A  C  e.  B  ->  ( E. x  e.  A  y  =  C  ->  E. x  e.  A  y  =  ( F `  x ) ) )
4645imp 431 . . . . . . 7  |-  ( ( A. x  e.  A  C  e.  B  /\  E. x  e.  A  y  =  C )  ->  E. x  e.  A  y  =  ( F `  x ) )
4733, 35, 46syl2anc 666 . . . . . 6  |-  ( ( ( A. x  e.  A  C  e.  B  /\  A. y  e.  B  E. x  e.  A  y  =  C )  /\  y  e.  B
)  ->  E. x  e.  A  y  =  ( F `  x ) )
4847ex 436 . . . . 5  |-  ( ( A. x  e.  A  C  e.  B  /\  A. y  e.  B  E. x  e.  A  y  =  C )  ->  (
y  e.  B  ->  E. x  e.  A  y  =  ( F `  x ) ) )
4932, 48ralrimi 2787 . . . 4  |-  ( ( A. x  e.  A  C  e.  B  /\  A. y  e.  B  E. x  e.  A  y  =  C )  ->  A. y  e.  B  E. x  e.  A  y  =  ( F `  x ) )
5029, 49jca 535 . . 3  |-  ( ( A. x  e.  A  C  e.  B  /\  A. y  e.  B  E. x  e.  A  y  =  C )  ->  ( F : A --> B  /\  A. y  e.  B  E. x  e.  A  y  =  ( F `  x ) ) )
5150, 4sylibr 216 . 2  |-  ( ( A. x  e.  A  C  e.  B  /\  A. y  e.  B  E. x  e.  A  y  =  C )  ->  F : A -onto-> B )
5227, 51impbii 191 1  |-  ( F : A -onto-> B  <->  ( A. x  e.  A  C  e.  B  /\  A. y  e.  B  E. x  e.  A  y  =  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 984    = wceq 1443    e. wcel 1886   A.wral 2736   E.wrex 2737    |-> cmpt 4460   -->wf 5577   -onto->wfo 5579   ` cfv 5581
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-fo 5587  df-fv 5589
This theorem is referenced by:  disjinfi  37462
  Copyright terms: Public domain W3C validator