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		iunexg	⊢ ( ( 𝐶 ∈ V ∧ ∀ 𝑓 ∈ 𝐶 ran 𝑓 ∈ V ) → ∪ 𝑓 ∈ 𝐶 ran 𝑓 ∈ V )
15	11 13 14	sylancl	⊢ ( 𝜑 → ∪ 𝑓 ∈ 𝐶 ran 𝑓 ∈ V )
16	9 15	eqeltrd	⊢ ( 𝜑 → 𝐷 ∈ V )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → 𝐷 ∈ V )
18		ssiun2	⊢ ( 𝑓 ∈ 𝐶 → ran 𝑓 ⊆ ∪ 𝑓 ∈ 𝐶 ran 𝑓 )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ran 𝑓 ⊆ ∪ 𝑓 ∈ 𝐶 ran 𝑓 )
20		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
21	2 20	syl	⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → 𝐴 ∈ { 𝐴 } )
23	8 22	fnfvelrnd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑓 )
24	19 23	sseldd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( 𝑓 ‘ 𝐴 ) ∈ ∪ 𝑓 ∈ 𝐶 ran 𝑓 )
25	24 4	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( 𝑓 ‘ 𝐴 ) ∈ 𝐷 )
26	8 17 25	elmapsnd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) )
27	16	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → 𝐷 ∈ V )
28		snex	⊢ { 𝐴 } ∈ V
29	28	a1i	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → { 𝐴 } ∈ V )
30		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) )
31	21	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → 𝐴 ∈ { 𝐴 } )
32	27 29 30 31	fvmap	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → ( 𝑓 ‘ 𝐴 ) ∈ 𝐷 )
33		rneq	⊢ ( 𝑓 = 𝑔 → ran 𝑓 = ran 𝑔 )
34	33	cbviunv	⊢ ∪ 𝑓 ∈ 𝐶 ran 𝑓 = ∪ 𝑔 ∈ 𝐶 ran 𝑔
35	4 34	eqtri	⊢ 𝐷 = ∪ 𝑔 ∈ 𝐶 ran 𝑔
36	32 35	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → ( 𝑓 ‘ 𝐴 ) ∈ ∪ 𝑔 ∈ 𝐶 ran 𝑔 )
37		eliun	⊢ ( ( 𝑓 ‘ 𝐴 ) ∈ ∪ 𝑔 ∈ 𝐶 ran 𝑔 ↔ ∃ 𝑔 ∈ 𝐶 ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 )
38	36 37	sylib	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → ∃ 𝑔 ∈ 𝐶 ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 )
39		simp3	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 )
40		simp1l	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝜑 )
41	40 2	syl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝐴 ∈ 𝑉 )
42		eqid	⊢ { 𝐴 } = { 𝐴 }
43		simp1r	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) )
44		elmapfn	⊢ ( 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) → 𝑓 Fn { 𝐴 } )
45	43 44	syl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝑓 Fn { 𝐴 } )
46	3	sselda	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ) → 𝑔 ∈ ( 𝐵 ↑m { 𝐴 } ) )
47		elmapfn	⊢ ( 𝑔 ∈ ( 𝐵 ↑m { 𝐴 } ) → 𝑔 Fn { 𝐴 } )
48	46 47	syl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ) → 𝑔 Fn { 𝐴 } )
49	48	3adant3	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝑔 Fn { 𝐴 } )
50	49	3adant1r	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝑔 Fn { 𝐴 } )
51	41 42 45 50	fsneqrn	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → ( 𝑓 = 𝑔 ↔ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) )
52	39 51	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝑓 = 𝑔 )
53		simp2	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝑔 ∈ 𝐶 )
54	52 53	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) ∧ 𝑔 ∈ 𝐶 ∧ ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 ) → 𝑓 ∈ 𝐶 )
55	54	rexlimdv3a	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → ( ∃ 𝑔 ∈ 𝐶 ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑔 → 𝑓 ∈ 𝐶 ) )
56	38 55	mpd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) → 𝑓 ∈ 𝐶 )
57	26 56	impbida	⊢ ( 𝜑 → ( 𝑓 ∈ 𝐶 ↔ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) )
58	57	alrimiv	⊢ ( 𝜑 → ∀ 𝑓 ( 𝑓 ∈ 𝐶 ↔ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) )
59		nfcv	⊢ Ⅎ 𝑓 𝐶
60		nfcv	⊢ Ⅎ 𝑓 ↑m
61		nfcv	⊢ Ⅎ 𝑓 { 𝐴 }
62	1 60 61	nfov	⊢ Ⅎ 𝑓 ( 𝐷 ↑m { 𝐴 } )
63	59 62	cleqf	⊢ ( 𝐶 = ( 𝐷 ↑m { 𝐴 } ) ↔ ∀ 𝑓 ( 𝑓 ∈ 𝐶 ↔ 𝑓 ∈ ( 𝐷 ↑m { 𝐴 } ) ) )
64	58 63	sylibr	⊢ ( 𝜑 → 𝐶 = ( 𝐷 ↑m { 𝐴 } ) )