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

Metamath Proof Explorer

Theorem snelmap

Description: Membership of the element in the range of a constant map. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses snelmap.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
snelmap.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
snelmap.n ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
snelmap.e ⊢ ( 𝜑 → ( 𝐴 × { 𝑥 } ) ∈ ( 𝐵 ↑m 𝐴 ) )
Assertion snelmap ( 𝜑 → 𝑥 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 snelmap.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 snelmap.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 snelmap.n ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
4 snelmap.e ⊢ ( 𝜑 → ( 𝐴 × { 𝑥 } ) ∈ ( 𝐵 ↑m 𝐴 ) )
5 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐴 )
6 3 5 sylib ⊢ ( 𝜑 → ∃ 𝑦 𝑦 ∈ 𝐴 )
7 vex ⊢ 𝑥 ∈ V
8 7 fvconst2 ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝐴 × { 𝑥 } ) ‘ 𝑦 ) = 𝑥 )
9 8 eqcomd ⊢ ( 𝑦 ∈ 𝐴 → 𝑥 = ( ( 𝐴 × { 𝑥 } ) ‘ 𝑦 ) )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 = ( ( 𝐴 × { 𝑥 } ) ‘ 𝑦 ) )
11 elmapg ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 × { 𝑥 } ) ∈ ( 𝐵 ↑m 𝐴 ) ↔ ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ 𝐵 ) )
12 2 1 11 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 × { 𝑥 } ) ∈ ( 𝐵 ↑m 𝐴 ) ↔ ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ 𝐵 ) )
13 4 12 mpbid ⊢ ( 𝜑 → ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ 𝐵 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ 𝐵 )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
16 14 15 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐴 × { 𝑥 } ) ‘ 𝑦 ) ∈ 𝐵 )
17 10 16 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
18 17 ex ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
19 18 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑦 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
20 6 19 mpd ⊢ ( 𝜑 → 𝑥 ∈ 𝐵 )