ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fiss Unicode version

Theorem fiss 6966
Description: Subset relationship for function  fi. (Contributed by Jeff Hankins, 7-Oct-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
Assertion
Ref Expression
fiss  |-  ( ( B  e.  V  /\  A  C_  B )  -> 
( fi `  A
)  C_  ( fi `  B ) )

Proof of Theorem fiss
Dummy variables  r  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 110 . . . 4  |-  ( ( B  e.  V  /\  A  C_  B )  ->  A  C_  B )
2 sspwb 4210 . . . . 5  |-  ( A 
C_  B  <->  ~P A  C_ 
~P B )
3 ssrin 3358 . . . . 5  |-  ( ~P A  C_  ~P B  ->  ( ~P A  i^i  Fin )  C_  ( ~P B  i^i  Fin ) )
42, 3sylbi 121 . . . 4  |-  ( A 
C_  B  ->  ( ~P A  i^i  Fin )  C_  ( ~P B  i^i  Fin ) )
5 ssrexv 3218 . . . 4  |-  ( ( ~P A  i^i  Fin )  C_  ( ~P B  i^i  Fin )  ->  ( E. x  e.  ( ~P A  i^i  Fin )
r  =  |^| x  ->  E. x  e.  ( ~P B  i^i  Fin ) r  =  |^| x ) )
61, 4, 53syl 17 . . 3  |-  ( ( B  e.  V  /\  A  C_  B )  -> 
( E. x  e.  ( ~P A  i^i  Fin ) r  =  |^| x  ->  E. x  e.  ( ~P B  i^i  Fin ) r  =  |^| x ) )
7 vex 2738 . . . 4  |-  r  e. 
_V
8 simpl 109 . . . . 5  |-  ( ( B  e.  V  /\  A  C_  B )  ->  B  e.  V )
98, 1ssexd 4138 . . . 4  |-  ( ( B  e.  V  /\  A  C_  B )  ->  A  e.  _V )
10 elfi 6960 . . . 4  |-  ( ( r  e.  _V  /\  A  e.  _V )  ->  ( r  e.  ( fi `  A )  <->  E. x  e.  ( ~P A  i^i  Fin )
r  =  |^| x
) )
117, 9, 10sylancr 414 . . 3  |-  ( ( B  e.  V  /\  A  C_  B )  -> 
( r  e.  ( fi `  A )  <->  E. x  e.  ( ~P A  i^i  Fin )
r  =  |^| x
) )
12 elfi 6960 . . . . 5  |-  ( ( r  e.  _V  /\  B  e.  V )  ->  ( r  e.  ( fi `  B )  <->  E. x  e.  ( ~P B  i^i  Fin )
r  =  |^| x
) )
137, 12mpan 424 . . . 4  |-  ( B  e.  V  ->  (
r  e.  ( fi
`  B )  <->  E. x  e.  ( ~P B  i^i  Fin ) r  =  |^| x ) )
1413adantr 276 . . 3  |-  ( ( B  e.  V  /\  A  C_  B )  -> 
( r  e.  ( fi `  B )  <->  E. x  e.  ( ~P B  i^i  Fin )
r  =  |^| x
) )
156, 11, 143imtr4d 203 . 2  |-  ( ( B  e.  V  /\  A  C_  B )  -> 
( r  e.  ( fi `  A )  ->  r  e.  ( fi `  B ) ) )
1615ssrdv 3159 1  |-  ( ( B  e.  V  /\  A  C_  B )  -> 
( fi `  A
)  C_  ( fi `  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    = wceq 1353    e. wcel 2146   E.wrex 2454   _Vcvv 2735    i^i cin 3126    C_ wss 3127   ~Pcpw 3572   |^|cint 3840   ` cfv 5208   Fincfn 6730   ficfi 6957
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-nul 4124  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-iinf 4581
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-ral 2458  df-rex 2459  df-v 2737  df-sbc 2961  df-csb 3056  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-nul 3421  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-br 3999  df-opab 4060  df-mpt 4061  df-id 4287  df-suc 4365  df-iom 4584  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-f1 5213  df-fo 5214  df-f1o 5215  df-fv 5216  df-er 6525  df-en 6731  df-fin 6733  df-fi 6958
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator