This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 { 𝐴 } ) )