Theorem 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	⊢ Ⅎ 𝑓 𝐷
	ssmapsn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ssmapsn.c	⊢ ( 𝜑 → 𝐶 ⊆ ( 𝐵 ↑m { 𝐴 } ) )
	ssmapsn.d	⊢ 𝐷 = ∪ 𝑓 ∈ 𝐶 ran 𝑓
Assertion	ssmapsn	⊢ ( 𝜑 → 𝐶 = ( 𝐷 ↑m { 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		ssmapsn.f	⊢ Ⅎ 𝑓 𝐷
2		ssmapsn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		ssmapsn.c	⊢ ( 𝜑 → 𝐶 ⊆ ( 𝐵 ↑m { 𝐴 } ) )
4		ssmapsn.d	⊢ 𝐷 = ∪ 𝑓 ∈ 𝐶 ran 𝑓
5	3	sselda	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → 𝑓 ∈ ( 𝐵 ↑m { 𝐴 } ) )
6		elmapi	⊢ ( 𝑓 ∈ ( 𝐵 ↑m { 𝐴 } ) → 𝑓 : { 𝐴 } ⟶ 𝐵 )
7	5 6	syl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → 𝑓 : { 𝐴 } ⟶ 𝐵 )
8	7	ffnd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → 𝑓 Fn { 𝐴 } )
9	4	a1i	⊢ ( 𝜑 → 𝐷 = ∪ 𝑓 ∈ 𝐶 ran 𝑓 )
10		ovexd	⊢ ( 𝜑 → ( 𝐵 ↑m { 𝐴 } ) ∈ V )
11	10 3	ssexd	⊢ ( 𝜑 → 𝐶 ∈ V )
12		rnexg	⊢ ( 𝑓 ∈ 𝐶 → ran 𝑓 ∈ V )
13	12	rgen	⊢ ∀ 𝑓 ∈ 𝐶 ran 𝑓 ∈ V
14	13	a1i	⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝐶 ran 𝑓 ∈ V )
15	11 14	jca	⊢ ( 𝜑 → ( 𝐶 ∈ V ∧ ∀ 𝑓 ∈ 𝐶 ran 𝑓 ∈ V ) )
16		iunexg	⊢ ( ( 𝐶 ∈ V ∧ ∀ 𝑓 ∈ 𝐶 ran 𝑓 ∈ V ) → ∪ 𝑓 ∈ 𝐶 ran 𝑓 ∈ V )
17	15 16	syl	⊢ ( 𝜑 → ∪ 𝑓 ∈ 𝐶 ran 𝑓 ∈ V )
18	9 17	eqeltrd	⊢ ( 𝜑 → 𝐷 ∈ V )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → 𝐷 ∈ V )
20		ssiun2	⊢ ( 𝑓 ∈ 𝐶 → ran 𝑓 ⊆ ∪ 𝑓 ∈ 𝐶 ran 𝑓 )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ran 𝑓 ⊆ ∪ 𝑓 ∈ 𝐶 ran 𝑓 )
22		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
23	2 22	syl	⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → 𝐴 ∈ { 𝐴 } )
25		fnfvelrn	⊢ ( ( 𝑓 Fn { 𝐴 } ∧ 𝐴 ∈ { 𝐴 } ) → ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑓 )
26	8 24 25	syl2anc	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑓 )
27	21 26	sseldd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( 𝑓 ‘ 𝐴 ) ∈ ∪ 𝑓 ∈ 𝐶 ran 𝑓 )
28	27 4	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( 𝑓 ‘ 𝐴 ) ∈ 𝐷 )
29	8 19 28	elmapsnd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) )
30	29	ex	⊢ ( 𝜑 → ( 𝑓 ∈ 𝐶 → 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) )
31	18	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → 𝐷 ∈ V )
32		snex	⊢ { 𝐴 } ∈ V
33	32	a1i	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → { 𝐴 } ∈ V )
34		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) )
35	23	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → 𝐴 ∈ { 𝐴 } )
36	31 33 34 35	fvmap	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → ( 𝑓 ‘ 𝐴 ) ∈ 𝐷 )
37	4	idi	⊢ 𝐷 = ∪ 𝑓 ∈ 𝐶 ran 𝑓
38		rneq	⊢ ( 𝑓 = 𝑔 → ran 𝑓 = ran 𝑔 )
39	38	cbviunv	⊢ ∪ 𝑓 ∈ 𝐶 ran 𝑓 = ∪ 𝑔 ∈ 𝐶 ran 𝑔
40	37 39	eqtri	⊢ 𝐷 = ∪ 𝑔 ∈ 𝐶 ran 𝑔
41	36 40	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → ( 𝑓 ‘ 𝐴 ) ∈ ∪ 𝑔 ∈ 𝐶 ran 𝑔 )
42		eliun	⊢ ( ( 𝑓 ‘ 𝐴 ) ∈ ∪ 𝑔 ∈ 𝐶 ran 𝑔 ↔ ∃ 𝑔 ∈ 𝐶 ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 )
43	41 42	sylib	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → ∃ 𝑔 ∈ 𝐶 ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 )
44		simp3	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 )
45		simp1l	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝜑 )
46	45 2	syl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝐴 ∈ 𝑉 )
47		eqid	⊢ { 𝐴 } = { 𝐴 }
48		simp1r	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) )
49		elmapfn	⊢ ( 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) → 𝑓 Fn { 𝐴 } )
50	48 49	syl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝑓 Fn { 𝐴 } )
51	3	sselda	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ) → 𝑔 ∈ ( 𝐵 ↑m { 𝐴 } ) )
52		elmapfn	⊢ ( 𝑔 ∈ ( 𝐵 ↑m { 𝐴 } ) → 𝑔 Fn { 𝐴 } )
53	51 52	syl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ) → 𝑔 Fn { 𝐴 } )
54	53	3adant3	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝑔 Fn { 𝐴 } )
55	54	3adant1r	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝑔 Fn { 𝐴 } )
56	46 47 50 55	fsneqrn	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → ( 𝑓 = 𝑔 ↔ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) )
57	44 56	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝑓 = 𝑔 )
58		simp2	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝑔 ∈ 𝐶 )
59	57 58	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝑓 ∈ 𝐶 )
60	59	3exp	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → ( 𝑔 ∈ 𝐶 → ( ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 → 𝑓 ∈ 𝐶 ) ) )
61	60	rexlimdv	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → ( ∃ 𝑔 ∈ 𝐶 ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 → 𝑓 ∈ 𝐶 ) )
62	43 61	mpd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → 𝑓 ∈ 𝐶 )
63	62	ex	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) → 𝑓 ∈ 𝐶 ) )
64	30 63	impbid	⊢ ( 𝜑 → ( 𝑓 ∈ 𝐶 ↔ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) )
65	64	alrimiv	⊢ ( 𝜑 → ∀ 𝑓 ( 𝑓 ∈ 𝐶 ↔ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) )
66		nfcv	⊢ Ⅎ 𝑓 𝐶
67		nfcv	⊢ Ⅎ 𝑓 ↑m
68		nfcv	⊢ Ⅎ 𝑓 { 𝐴 }
69	1 67 68	nfov	⊢ Ⅎ 𝑓 ( 𝐷 ↑m { 𝐴 } )
70	66 69	cleqf	⊢ ( 𝐶 = ( 𝐷 ↑m { 𝐴 } ) ↔ ∀ 𝑓 ( 𝑓 ∈ 𝐶 ↔ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) )
71	65 70	sylibr	⊢ ( 𝜑 → 𝐶 = ( 𝐷 ↑m { 𝐴 } ) )