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 ⊢ φ → A ∈ On
cantnfs.b ⊢ φ → B ∈ On
Assertion cantnfs ⊢ φ → F ∈ S ↔ F : B ⟶ A ∧ finSupp ∅⁡ F

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ S = dom ⁡ A CNF B
2 cantnfs.a ⊢ φ → A ∈ On
3 cantnfs.b ⊢ φ → B ∈ On
4 eqid ⊢ g ∈ A B | finSupp ∅⁡ g = g ∈ A B | finSupp ∅⁡ g
5 4 2 3 cantnfdm ⊢ φ → dom ⁡ A CNF B = g ∈ A B | finSupp ∅⁡ g
6 1 5 eqtrid ⊢ φ → S = g ∈ A B | finSupp ∅⁡ g
7 6 eleq2d ⊢ φ → F ∈ S ↔ F ∈ g ∈ A B | finSupp ∅⁡ g
8 breq1 ⊢ g = F → finSupp ∅⁡ g ↔ finSupp ∅⁡ F
9 8 elrab ⊢ F ∈ g ∈ A B | finSupp ∅⁡ g ↔ F ∈ A B ∧ finSupp ∅⁡ F
10 7 9 bitrdi ⊢ φ → F ∈ S ↔ F ∈ A B ∧ finSupp ∅⁡ F
11 2 3 elmapd ⊢ φ → F ∈ A B ↔ F : B ⟶ A
12 11 anbi1d ⊢ φ → F ∈ A B ∧ finSupp ∅⁡ F ↔ F : B ⟶ A ∧ finSupp ∅⁡ F
13 10 12 bitrd ⊢ φ → F ∈ S ↔ F : B ⟶ A ∧ finSupp ∅⁡ F