This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cantnfs

Description: Elementhood in the set of finitely supported functions from B to A . (Contributed by Mario Carneiro, 25-May-2015) (Revised by AV, 28-Jun-2019)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
Assertion cantnfs 
|- ( ph -> ( F e. S <-> ( F : B --> A /\ F finSupp (/) ) ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s 
 |-  S = dom ( A CNF B )
2 cantnfs.a 
 |-  ( ph -> A e. On )
3 cantnfs.b 
 |-  ( ph -> B e. On )
4 eqid 
 |-  { g e. ( A ^m B ) | g finSupp (/) } = { g e. ( A ^m B ) | g finSupp (/) }
5 4 2 3 cantnfdm 
 |-  ( ph -> dom ( A CNF B ) = { g e. ( A ^m B ) | g finSupp (/) } )
6 1 5 eqtrid 
 |-  ( ph -> S = { g e. ( A ^m B ) | g finSupp (/) } )
7 6 eleq2d 
 |-  ( ph -> ( F e. S <-> F e. { g e. ( A ^m B ) | g finSupp (/) } ) )
8 breq1 
 |-  ( g = F -> ( g finSupp (/) <-> F finSupp (/) ) )
9 8 elrab 
 |-  ( F e. { g e. ( A ^m B ) | g finSupp (/) } <-> ( F e. ( A ^m B ) /\ F finSupp (/) ) )
10 7 9 bitrdi 
 |-  ( ph -> ( F e. S <-> ( F e. ( A ^m B ) /\ F finSupp (/) ) ) )
11 2 3 elmapd 
 |-  ( ph -> ( F e. ( A ^m B ) <-> F : B --> A ) )
12 11 anbi1d 
 |-  ( ph -> ( ( F e. ( A ^m B ) /\ F finSupp (/) ) <-> ( F : B --> A /\ F finSupp (/) ) ) )
13 10 12 bitrd 
 |-  ( ph -> ( F e. S <-> ( F : B --> A /\ F finSupp (/) ) ) )