ssmapsn

Description: A subset C of a set exponentiation to a singleton, is its projection D exponentiated to the singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ssmapsn.f	$⊢ \underline{Ⅎ} f D$
	ssmapsn.a	$⊢ φ \to A \in V$
	ssmapsn.c	$⊢ φ \to C \subseteq B^{\{A\}}$
	ssmapsn.d	$⊢ D = ⋃_{f \in C} ran f$
Assertion	ssmapsn	$⊢ φ \to C = D^{\{A\}}$

Proof

Step	Hyp	Ref	Expression
1		ssmapsn.f	$⊢ \underline{Ⅎ} f D$
2		ssmapsn.a	$⊢ φ \to A \in V$
3		ssmapsn.c	$⊢ φ \to C \subseteq B^{\{A\}}$
4		ssmapsn.d	$⊢ D = ⋃_{f \in C} ran f$
5	3	sselda	$⊢ (φ \land f \in C) \to f \in (B^{\{A\}})$
6		elmapi	$⊢ f \in (B^{\{A\}}) \to f : \{A\} ⟶ B$
7	5 6	syl	$⊢ (φ \land f \in C) \to f : \{A\} ⟶ B$
8	7	ffnd	$⊢ (φ \land f \in C) \to f Fn \{A\}$
9	4	a1i	$⊢ φ \to D = ⋃_{f \in C} ran f$
10		ovexd	$⊢ φ \to B^{\{A\}} \in V$
11	10 3	ssexd	$⊢ φ \to C \in V$
12		rnexg	$⊢ f \in C \to ran f \in V$
13	12	rgen	$⊢ \forall f \in C ran f \in V$
14		iunexg	$⊢ (C \in V \land \forall f \in C ran f \in V) \to ⋃_{f \in C} ran f \in V$
15	11 13 14	sylancl	$⊢ φ \to ⋃_{f \in C} ran f \in V$
16	9 15	eqeltrd	$⊢ φ \to D \in V$
17	16	adantr	$⊢ (φ \land f \in C) \to D \in V$
18		ssiun2	$⊢ f \in C \to ran f \subseteq ⋃_{f \in C} ran f$
19	18	adantl	$⊢ (φ \land f \in C) \to ran f \subseteq ⋃_{f \in C} ran f$
20		snidg	$⊢ A \in V \to A \in \{A\}$
21	2 20	syl	$⊢ φ \to A \in \{A\}$
22	21	adantr	$⊢ (φ \land f \in C) \to A \in \{A\}$
23	8 22	fnfvelrnd	$⊢ (φ \land f \in C) \to f (A) \in ran f$
24	19 23	sseldd	$⊢ (φ \land f \in C) \to f (A) \in ⋃_{f \in C} ran f$
25	24 4	eleqtrrdi	$⊢ (φ \land f \in C) \to f (A) \in D$
26	8 17 25	elmapsnd	$⊢ (φ \land f \in C) \to f \in (D^{\{A\}})$
27	16	adantr	$⊢ (φ \land f \in (D^{\{A\}})) \to D \in V$
28		snex	$⊢ \{A\} \in V$
29	28	a1i	$⊢ (φ \land f \in (D^{\{A\}})) \to \{A\} \in V$
30		simpr	$⊢ (φ \land f \in (D^{\{A\}})) \to f \in (D^{\{A\}})$
31	21	adantr	$⊢ (φ \land f \in (D^{\{A\}})) \to A \in \{A\}$
32	27 29 30 31	fvmap	$⊢ (φ \land f \in (D^{\{A\}})) \to f (A) \in D$
33		rneq	$⊢ f = g \to ran f = ran g$
34	33	cbviunv	$⊢ ⋃_{f \in C} ran f = ⋃_{g \in C} ran g$
35	4 34	eqtri	$⊢ D = ⋃_{g \in C} ran g$
36	32 35	eleqtrdi	$⊢ (φ \land f \in (D^{\{A\}})) \to f (A) \in ⋃_{g \in C} ran g$
37		eliun	$⊢ f (A) \in ⋃_{g \in C} ran g \leftrightarrow \exists g \in C f (A) \in ran g$
38	36 37	sylib	$⊢ (φ \land f \in (D^{\{A\}})) \to \exists g \in C f (A) \in ran g$
39		simp3	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to f (A) \in ran g$
40		simp1l	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to φ$
41	40 2	syl	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to A \in V$
42		eqid	$⊢ \{A\} = \{A\}$
43		simp1r	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to f \in (D^{\{A\}})$
44		elmapfn	$⊢ f \in (D^{\{A\}}) \to f Fn \{A\}$
45	43 44	syl	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to f Fn \{A\}$
46	3	sselda	$⊢ (φ \land g \in C) \to g \in (B^{\{A\}})$
47		elmapfn	$⊢ g \in (B^{\{A\}}) \to g Fn \{A\}$
48	46 47	syl	$⊢ (φ \land g \in C) \to g Fn \{A\}$
49	48	3adant3	$⊢ (φ \land g \in C \land f (A) \in ran g) \to g Fn \{A\}$
50	49	3adant1r	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to g Fn \{A\}$
51	41 42 45 50	fsneqrn	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to (f = g \leftrightarrow f (A) \in ran g)$
52	39 51	mpbird	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to f = g$
53		simp2	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to g \in C$
54	52 53	eqeltrd	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to f \in C$
55	54	rexlimdv3a	$⊢ (φ \land f \in (D^{\{A\}})) \to (\exists g \in C f (A) \in ran g \to f \in C)$
56	38 55	mpd	$⊢ (φ \land f \in (D^{\{A\}})) \to f \in C$
57	26 56	impbida	$⊢ φ \to (f \in C \leftrightarrow f \in (D^{\{A\}}))$
58	57	alrimiv	$⊢ φ \to \forall f (f \in C \leftrightarrow f \in (D^{\{A\}}))$
59		nfcv	$⊢ \underline{Ⅎ} f C$
60		nfcv	$⊢ \underline{Ⅎ} f ↑_{𝑚}$
61		nfcv	$⊢ \underline{Ⅎ} f \{A\}$
62	1 60 61	nfov	$⊢ \underline{Ⅎ} f (D^{\{A\}})$
63	59 62	cleqf	$⊢ C = D^{\{A\}} \leftrightarrow \forall f (f \in C \leftrightarrow f \in (D^{\{A\}}))$
64	58 63	sylibr	$⊢ φ \to C = D^{\{A\}}$

Metamath Proof Explorer

Theorem ssmapsn

Proof