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

Metamath Proof Explorer

Theorem fmptsnd

Description: Express a singleton function in maps-to notation. Deduction form of fmptsng . (Contributed by AV, 4-Aug-2019)

Ref Expression
Hypotheses fmptsnd.1 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 = 𝐶 )
fmptsnd.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
fmptsnd.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
Assertion fmptsnd ( 𝜑 → { ⟨ 𝐴 , 𝐶 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fmptsnd.1 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 = 𝐶 )
2 fmptsnd.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 fmptsnd.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
4 velsn ⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
5 4 bicomi ⊢ ( 𝑥 = 𝐴 ↔ 𝑥 ∈ { 𝐴 } )
6 5 anbi1i ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 = 𝐵 ) )
7 6 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 = 𝐵 ) }
8 velsn ⊢ ( 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ↔ 𝑝 = ⟨ 𝐴 , 𝐶 ⟩ )
9 eqidd ⊢ ( 𝜑 → 𝐴 = 𝐴 )
10 eqidd ⊢ ( 𝜑 → 𝐶 = 𝐶 )
11 sbcan ⊢ ( [ 𝐶 / 𝑦 ] ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( [ 𝐶 / 𝑦 ] 𝑥 = 𝐴 ∧ [ 𝐶 / 𝑦 ] 𝑦 = 𝐵 ) )
12 sbcg ⊢ ( 𝐶 ∈ 𝑊 → ( [ 𝐶 / 𝑦 ] 𝑥 = 𝐴 ↔ 𝑥 = 𝐴 ) )
13 3 12 syl ⊢ ( 𝜑 → ( [ 𝐶 / 𝑦 ] 𝑥 = 𝐴 ↔ 𝑥 = 𝐴 ) )
14 eqsbc1 ⊢ ( 𝐶 ∈ 𝑊 → ( [ 𝐶 / 𝑦 ] 𝑦 = 𝐵 ↔ 𝐶 = 𝐵 ) )
15 3 14 syl ⊢ ( 𝜑 → ( [ 𝐶 / 𝑦 ] 𝑦 = 𝐵 ↔ 𝐶 = 𝐵 ) )
16 13 15 anbi12d ⊢ ( 𝜑 → ( ( [ 𝐶 / 𝑦 ] 𝑥 = 𝐴 ∧ [ 𝐶 / 𝑦 ] 𝑦 = 𝐵 ) ↔ ( 𝑥 = 𝐴 ∧ 𝐶 = 𝐵 ) ) )
17 11 16 bitrid ⊢ ( 𝜑 → ( [ 𝐶 / 𝑦 ] ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 = 𝐴 ∧ 𝐶 = 𝐵 ) ) )
18 17 sbcbidv ⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] [ 𝐶 / 𝑦 ] ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ [ 𝐴 / 𝑥 ] ( 𝑥 = 𝐴 ∧ 𝐶 = 𝐵 ) ) )
19 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝐴 ↔ 𝐴 = 𝐴 ) )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝑥 = 𝐴 ↔ 𝐴 = 𝐴 ) )
21 1 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝐶 = 𝐵 ↔ 𝐶 = 𝐶 ) )
22 20 21 anbi12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝑥 = 𝐴 ∧ 𝐶 = 𝐵 ) ↔ ( 𝐴 = 𝐴 ∧ 𝐶 = 𝐶 ) ) )
23 2 22 sbcied ⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] ( 𝑥 = 𝐴 ∧ 𝐶 = 𝐵 ) ↔ ( 𝐴 = 𝐴 ∧ 𝐶 = 𝐶 ) ) )
24 18 23 bitrd ⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] [ 𝐶 / 𝑦 ] ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝐴 = 𝐴 ∧ 𝐶 = 𝐶 ) ) )
25 9 10 24 mpbir2and ⊢ ( 𝜑 → [ 𝐴 / 𝑥 ] [ 𝐶 / 𝑦 ] ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
26 opelopabsb ⊢ ( ⟨ 𝐴 , 𝐶 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ↔ [ 𝐴 / 𝑥 ] [ 𝐶 / 𝑦 ] ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
27 25 26 sylibr ⊢ ( 𝜑 → ⟨ 𝐴 , 𝐶 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } )
28 eleq1 ⊢ ( 𝑝 = ⟨ 𝐴 , 𝐶 ⟩ → ( 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ↔ ⟨ 𝐴 , 𝐶 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ) )
29 27 28 syl5ibrcom ⊢ ( 𝜑 → ( 𝑝 = ⟨ 𝐴 , 𝐶 ⟩ → 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ) )
30 8 29 biimtrid ⊢ ( 𝜑 → ( 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } → 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ) )
31 elopab ⊢ ( 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) )
32 opeq12 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
33 32 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
34 33 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ ) )
35 1 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝐵 = 𝐶 )
36 35 opeq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐶 ⟩ )
37 opex ⊢ ⟨ 𝐴 , 𝐶 ⟩ ∈ V
38 37 snid ⊢ ⟨ 𝐴 , 𝐶 ⟩ ∈ { ⟨ 𝐴 , 𝐶 ⟩ }
39 36 38 eqeltrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝐴 , 𝐶 ⟩ } )
40 eleq1 ⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
41 39 40 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
42 34 41 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
43 42 ex ⊢ ( 𝜑 → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ) ) )
44 43 impcomd ⊢ ( 𝜑 → ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
45 44 exlimdvv ⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
46 31 45 biimtrid ⊢ ( 𝜑 → ( 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } → 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
47 30 46 impbid ⊢ ( 𝜑 → ( 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ↔ 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ) )
48 47 eqrdv ⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐶 ⟩ } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } )
49 df-mpt ⊢ ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 = 𝐵 ) }
50 49 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 = 𝐵 ) } )
51 7 48 50 3eqtr4a ⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐶 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) )