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

Metamath Proof Explorer

Theorem mapsnd

Description: The value of set exponentiation with a singleton exponent. Theorem 98 of Suppes p. 89. (Contributed by NM, 10-Dec-2003) (Revised by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses mapsnd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
mapsnd.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion mapsnd ( 𝜑 → ( 𝐴 ↑m { 𝐵 } ) = { 𝑓 ∣ ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } } )

Proof

Step Hyp Ref Expression
1 mapsnd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 mapsnd.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 snex ⊢ { 𝐵 } ∈ V
4 3 a1i ⊢ ( 𝜑 → { 𝐵 } ∈ V )
5 1 4 elmapd ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐴 ↑m { 𝐵 } ) ↔ 𝑓 : { 𝐵 } ⟶ 𝐴 ) )
6 ffn ⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → 𝑓 Fn { 𝐵 } )
7 snidg ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ { 𝐵 } )
8 2 7 syl ⊢ ( 𝜑 → 𝐵 ∈ { 𝐵 } )
9 fneu ⊢ ( ( 𝑓 Fn { 𝐵 } ∧ 𝐵 ∈ { 𝐵 } ) → ∃! 𝑦 𝐵 𝑓 𝑦 )
10 6 8 9 syl2anr ⊢ ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) → ∃! 𝑦 𝐵 𝑓 𝑦 )
11 euabsn ⊢ ( ∃! 𝑦 𝐵 𝑓 𝑦 ↔ ∃ 𝑦 { 𝑦 ∣ 𝐵 𝑓 𝑦 } = { 𝑦 } )
12 frel ⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → Rel 𝑓 )
13 relimasn ⊢ ( Rel 𝑓 → ( 𝑓 “ { 𝐵 } ) = { 𝑦 ∣ 𝐵 𝑓 𝑦 } )
14 12 13 syl ⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( 𝑓 “ { 𝐵 } ) = { 𝑦 ∣ 𝐵 𝑓 𝑦 } )
15 fdm ⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → dom 𝑓 = { 𝐵 } )
16 15 imaeq2d ⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( 𝑓 “ dom 𝑓 ) = ( 𝑓 “ { 𝐵 } ) )
17 imadmrn ⊢ ( 𝑓 “ dom 𝑓 ) = ran 𝑓
18 16 17 eqtr3di ⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( 𝑓 “ { 𝐵 } ) = ran 𝑓 )
19 14 18 eqtr3d ⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → { 𝑦 ∣ 𝐵 𝑓 𝑦 } = ran 𝑓 )
20 19 eqeq1d ⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( { 𝑦 ∣ 𝐵 𝑓 𝑦 } = { 𝑦 } ↔ ran 𝑓 = { 𝑦 } ) )
21 20 exbidv ⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( ∃ 𝑦 { 𝑦 ∣ 𝐵 𝑓 𝑦 } = { 𝑦 } ↔ ∃ 𝑦 ran 𝑓 = { 𝑦 } ) )
22 11 21 bitrid ⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( ∃! 𝑦 𝐵 𝑓 𝑦 ↔ ∃ 𝑦 ran 𝑓 = { 𝑦 } ) )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) → ( ∃! 𝑦 𝐵 𝑓 𝑦 ↔ ∃ 𝑦 ran 𝑓 = { 𝑦 } ) )
24 10 23 mpbid ⊢ ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) → ∃ 𝑦 ran 𝑓 = { 𝑦 } )
25 frn ⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ran 𝑓 ⊆ 𝐴 )
26 25 sseld ⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( 𝑦 ∈ ran 𝑓 → 𝑦 ∈ 𝐴 ) )
27 vsnid ⊢ 𝑦 ∈ { 𝑦 }
28 eleq2 ⊢ ( ran 𝑓 = { 𝑦 } → ( 𝑦 ∈ ran 𝑓 ↔ 𝑦 ∈ { 𝑦 } ) )
29 27 28 mpbiri ⊢ ( ran 𝑓 = { 𝑦 } → 𝑦 ∈ ran 𝑓 )
30 26 29 impel ⊢ ( ( 𝑓 : { 𝐵 } ⟶ 𝐴 ∧ ran 𝑓 = { 𝑦 } ) → 𝑦 ∈ 𝐴 )
31 30 adantll ⊢ ( ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) ∧ ran 𝑓 = { 𝑦 } ) → 𝑦 ∈ 𝐴 )
32 ffrn ⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → 𝑓 : { 𝐵 } ⟶ ran 𝑓 )
33 feq3 ⊢ ( ran 𝑓 = { 𝑦 } → ( 𝑓 : { 𝐵 } ⟶ ran 𝑓 ↔ 𝑓 : { 𝐵 } ⟶ { 𝑦 } ) )
34 32 33 syl5ibcom ⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( ran 𝑓 = { 𝑦 } → 𝑓 : { 𝐵 } ⟶ { 𝑦 } ) )
35 34 imp ⊢ ( ( 𝑓 : { 𝐵 } ⟶ 𝐴 ∧ ran 𝑓 = { 𝑦 } ) → 𝑓 : { 𝐵 } ⟶ { 𝑦 } )
36 35 adantll ⊢ ( ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) ∧ ran 𝑓 = { 𝑦 } ) → 𝑓 : { 𝐵 } ⟶ { 𝑦 } )
37 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) ∧ ran 𝑓 = { 𝑦 } ) → 𝐵 ∈ 𝑊 )
38 vex ⊢ 𝑦 ∈ V
39 fsng ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝑦 ∈ V ) → ( 𝑓 : { 𝐵 } ⟶ { 𝑦 } ↔ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
40 37 38 39 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) ∧ ran 𝑓 = { 𝑦 } ) → ( 𝑓 : { 𝐵 } ⟶ { 𝑦 } ↔ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
41 36 40 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) ∧ ran 𝑓 = { 𝑦 } ) → 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } )
42 31 41 jca ⊢ ( ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) ∧ ran 𝑓 = { 𝑦 } ) → ( 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
43 42 ex ⊢ ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) → ( ran 𝑓 = { 𝑦 } → ( 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) ) )
44 43 eximdv ⊢ ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) → ( ∃ 𝑦 ran 𝑓 = { 𝑦 } → ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) ) )
45 24 44 mpd ⊢ ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) → ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
46 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
47 45 46 sylibr ⊢ ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) → ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } )
48 47 ex ⊢ ( 𝜑 → ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
49 f1osng ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝑦 ∈ V ) → { ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐵 } –1-1-onto→ { 𝑦 } )
50 2 38 49 sylancl ⊢ ( 𝜑 → { ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐵 } –1-1-onto→ { 𝑦 } )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → { ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐵 } –1-1-onto→ { 𝑦 } )
52 f1oeq1 ⊢ ( 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } → ( 𝑓 : { 𝐵 } –1-1-onto→ { 𝑦 } ↔ { ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐵 } –1-1-onto→ { 𝑦 } ) )
53 52 bicomd ⊢ ( 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } → ( { ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐵 } –1-1-onto→ { 𝑦 } ↔ 𝑓 : { 𝐵 } –1-1-onto→ { 𝑦 } ) )
54 53 adantl ⊢ ( ( 𝜑 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → ( { ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐵 } –1-1-onto→ { 𝑦 } ↔ 𝑓 : { 𝐵 } –1-1-onto→ { 𝑦 } ) )
55 51 54 mpbid ⊢ ( ( 𝜑 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → 𝑓 : { 𝐵 } –1-1-onto→ { 𝑦 } )
56 f1of ⊢ ( 𝑓 : { 𝐵 } –1-1-onto→ { 𝑦 } → 𝑓 : { 𝐵 } ⟶ { 𝑦 } )
57 55 56 syl ⊢ ( ( 𝜑 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → 𝑓 : { 𝐵 } ⟶ { 𝑦 } )
58 57 3adant2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → 𝑓 : { 𝐵 } ⟶ { 𝑦 } )
59 snssi ⊢ ( 𝑦 ∈ 𝐴 → { 𝑦 } ⊆ 𝐴 )
60 59 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → { 𝑦 } ⊆ 𝐴 )
61 58 60 fssd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → 𝑓 : { 𝐵 } ⟶ 𝐴 )
62 61 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } → 𝑓 : { 𝐵 } ⟶ 𝐴 ) )
63 48 62 impbid ⊢ ( 𝜑 → ( 𝑓 : { 𝐵 } ⟶ 𝐴 ↔ ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
64 5 63 bitrd ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐴 ↑m { 𝐵 } ) ↔ ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
65 64 eqabdv ⊢ ( 𝜑 → ( 𝐴 ↑m { 𝐵 } ) = { 𝑓 ∣ ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } } )