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	13	a1i	$⊢ φ \to \forall f \in C ran f \in V$
15	11 14	jca	$⊢ φ \to (C \in V \land \forall f \in C ran f \in V)$
16		iunexg	$⊢ (C \in V \land \forall f \in C ran f \in V) \to ⋃_{f \in C} ran f \in V$
17	15 16	syl	$⊢ φ \to ⋃_{f \in C} ran f \in V$
18	9 17	eqeltrd	$⊢ φ \to D \in V$
19	18	adantr	$⊢ (φ \land f \in C) \to D \in V$
20		ssiun2	$⊢ f \in C \to ran f \subseteq ⋃_{f \in C} ran f$
21	20	adantl	$⊢ (φ \land f \in C) \to ran f \subseteq ⋃_{f \in C} ran f$
22		snidg	$⊢ A \in V \to A \in \{A\}$
23	2 22	syl	$⊢ φ \to A \in \{A\}$
24	23	adantr	$⊢ (φ \land f \in C) \to A \in \{A\}$
25		fnfvelrn	$⊢ (f Fn \{A\} \land A \in \{A\}) \to f (A) \in ran f$
26	8 24 25	syl2anc	$⊢ (φ \land f \in C) \to f (A) \in ran f$
27	21 26	sseldd	$⊢ (φ \land f \in C) \to f (A) \in ⋃_{f \in C} ran f$
28	27 4	eleqtrrdi	$⊢ (φ \land f \in C) \to f (A) \in D$
29	8 19 28	elmapsnd	$⊢ (φ \land f \in C) \to f \in (D^{\{A\}})$
30	29	ex	$⊢ φ \to (f \in C \to f \in (D^{\{A\}}))$
31	18	adantr	$⊢ (φ \land f \in (D^{\{A\}})) \to D \in V$
32		snex	$⊢ \{A\} \in V$
33	32	a1i	$⊢ (φ \land f \in (D^{\{A\}})) \to \{A\} \in V$
34		simpr	$⊢ (φ \land f \in (D^{\{A\}})) \to f \in (D^{\{A\}})$
35	23	adantr	$⊢ (φ \land f \in (D^{\{A\}})) \to A \in \{A\}$
36	31 33 34 35	fvmap	$⊢ (φ \land f \in (D^{\{A\}})) \to f (A) \in D$
37	4	idi	$⊢ D = ⋃_{f \in C} ran f$
38		rneq	$⊢ f = g \to ran f = ran g$
39	38	cbviunv	$⊢ ⋃_{f \in C} ran f = ⋃_{g \in C} ran g$
40	37 39	eqtri	$⊢ D = ⋃_{g \in C} ran g$
41	36 40	eleqtrdi	$⊢ (φ \land f \in (D^{\{A\}})) \to f (A) \in ⋃_{g \in C} ran g$
42		eliun	$⊢ f (A) \in ⋃_{g \in C} ran g \leftrightarrow \exists g \in C f (A) \in ran g$
43	41 42	sylib	$⊢ (φ \land f \in (D^{\{A\}})) \to \exists g \in C f (A) \in ran g$
44		simp3	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to f (A) \in ran g$
45		simp1l	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to φ$
46	45 2	syl	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to A \in V$
47		eqid	$⊢ \{A\} = \{A\}$
48		simp1r	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to f \in (D^{\{A\}})$
49		elmapfn	$⊢ f \in (D^{\{A\}}) \to f Fn \{A\}$
50	48 49	syl	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to f Fn \{A\}$
51	3	sselda	$⊢ (φ \land g \in C) \to g \in (B^{\{A\}})$
52		elmapfn	$⊢ g \in (B^{\{A\}}) \to g Fn \{A\}$
53	51 52	syl	$⊢ (φ \land g \in C) \to g Fn \{A\}$
54	53	3adant3	$⊢ (φ \land g \in C \land f (A) \in ran g) \to g Fn \{A\}$
55	54	3adant1r	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to g Fn \{A\}$
56	46 47 50 55	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)$
57	44 56	mpbird	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to f = g$
58		simp2	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to g \in C$
59	57 58	eqeltrd	$⊢ ((φ \land f \in (D^{\{A\}})) \land g \in C \land f (A) \in ran g) \to f \in C$
60	59	3exp	$⊢ (φ \land f \in (D^{\{A\}})) \to (g \in C \to (f (A) \in ran g \to f \in C))$
61	60	rexlimdv	$⊢ (φ \land f \in (D^{\{A\}})) \to (\exists g \in C f (A) \in ran g \to f \in C)$
62	43 61	mpd	$⊢ (φ \land f \in (D^{\{A\}})) \to f \in C$
63	62	ex	$⊢ φ \to (f \in (D^{\{A\}}) \to f \in C)$
64	30 63	impbid	$⊢ φ \to (f \in C \leftrightarrow f \in (D^{\{A\}}))$
65	64	alrimiv	$⊢ φ \to \forall f (f \in C \leftrightarrow f \in (D^{\{A\}}))$
66		nfcv	$⊢ \underline{Ⅎ} f C$
67		nfcv	$⊢ \underline{Ⅎ} f ↑_{𝑚}$
68		nfcv	$⊢ \underline{Ⅎ} f \{A\}$
69	1 67 68	nfov	$⊢ \underline{Ⅎ} f (D^{\{A\}})$
70	66 69	cleqf	$⊢ C = D^{\{A\}} \leftrightarrow \forall f (f \in C \leftrightarrow f \in (D^{\{A\}}))$
71	65 70	sylibr	$⊢ φ \to C = D^{\{A\}}$

Metamath Proof Explorer

Theorem ssmapsn

Proof