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 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ( 𝜑𝐴 ∈ On )
cantnfs.b ( 𝜑𝐵 ∈ On )
Assertion cantnfs ( 𝜑 → ( 𝐹𝑆 ↔ ( 𝐹 : 𝐵𝐴𝐹 finSupp ∅ ) ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s 𝑆 = dom ( 𝐴 CNF 𝐵 )
2 cantnfs.a ( 𝜑𝐴 ∈ On )
3 cantnfs.b ( 𝜑𝐵 ∈ On )
4 eqid { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ } = { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ }
5 4 2 3 cantnfdm ( 𝜑 → dom ( 𝐴 CNF 𝐵 ) = { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ } )
6 1 5 eqtrid ( 𝜑𝑆 = { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ } )
7 6 eleq2d ( 𝜑 → ( 𝐹𝑆𝐹 ∈ { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ } ) )
8 breq1 ( 𝑔 = 𝐹 → ( 𝑔 finSupp ∅ ↔ 𝐹 finSupp ∅ ) )
9 8 elrab ( 𝐹 ∈ { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ } ↔ ( 𝐹 ∈ ( 𝐴m 𝐵 ) ∧ 𝐹 finSupp ∅ ) )
10 7 9 bitrdi ( 𝜑 → ( 𝐹𝑆 ↔ ( 𝐹 ∈ ( 𝐴m 𝐵 ) ∧ 𝐹 finSupp ∅ ) ) )
11 2 3 elmapd ( 𝜑 → ( 𝐹 ∈ ( 𝐴m 𝐵 ) ↔ 𝐹 : 𝐵𝐴 ) )
12 11 anbi1d ( 𝜑 → ( ( 𝐹 ∈ ( 𝐴m 𝐵 ) ∧ 𝐹 finSupp ∅ ) ↔ ( 𝐹 : 𝐵𝐴𝐹 finSupp ∅ ) ) )
13 10 12 bitrd ( 𝜑 → ( 𝐹𝑆 ↔ ( 𝐹 : 𝐵𝐴𝐹 finSupp ∅ ) ) )