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	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐴 × { 𝑥 } ) ‘ 𝑦 ) ∈ 𝐵 )
17	10 16	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
18	17	ex	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
19	18	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑦 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
20	6 19	mpd	⊢ ( 𝜑 → 𝑥 ∈ 𝐵 )