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	syl5bi	⊢ ( 𝜑 → ( 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } → 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ) )
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	syl5bi	⊢ ( 𝜑 → ( 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } → 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
47	30 46	impbid	⊢ ( 𝜑 → ( 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ↔ 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ) )
48	47	eqrdv	⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐶 ⟩ } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } )
49		df-mpt	⊢ ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 = 𝐵 ) }
50	49	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 = 𝐵 ) } )
51	7 48 50	3eqtr4a	⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐶 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) )