mapsncnv

Description: Expression for the inverse of the canonical map between a set and its set of singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypotheses	mapsncnv.s	⊢ 𝑆 = { 𝑋 }
	mapsncnv.b	⊢ 𝐵 ∈ V
	mapsncnv.x	⊢ 𝑋 ∈ V
	mapsncnv.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝐵 ↑_m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) )
Assertion	mapsncnv	⊢ ^◡ 𝐹 = ( 𝑦 ∈ 𝐵 ↦ ( 𝑆 × { 𝑦 } ) )

Proof

Step	Hyp	Ref	Expression
1		mapsncnv.s	⊢ 𝑆 = { 𝑋 }
2		mapsncnv.b	⊢ 𝐵 ∈ V
3		mapsncnv.x	⊢ 𝑋 ∈ V
4		mapsncnv.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝐵 ↑_m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) )
5		elmapi	⊢ ( 𝑥 ∈ ( 𝐵 ↑_m { 𝑋 } ) → 𝑥 : { 𝑋 } ⟶ 𝐵 )
6	3	snid	⊢ 𝑋 ∈ { 𝑋 }
7		ffvelcdm	⊢ ( ( 𝑥 : { 𝑋 } ⟶ 𝐵 ∧ 𝑋 ∈ { 𝑋 } ) → ( 𝑥 ‘ 𝑋 ) ∈ 𝐵 )
8	5 6 7	sylancl	⊢ ( 𝑥 ∈ ( 𝐵 ↑_m { 𝑋 } ) → ( 𝑥 ‘ 𝑋 ) ∈ 𝐵 )
9		eqid	⊢ { 𝑋 } = { 𝑋 }
10	9 2 3	mapsnconst	⊢ ( 𝑥 ∈ ( 𝐵 ↑_m { 𝑋 } ) → 𝑥 = ( { 𝑋 } × { ( 𝑥 ‘ 𝑋 ) } ) )
11	8 10	jca	⊢ ( 𝑥 ∈ ( 𝐵 ↑_m { 𝑋 } ) → ( ( 𝑥 ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑥 = ( { 𝑋 } × { ( 𝑥 ‘ 𝑋 ) } ) ) )
12		eleq1	⊢ ( 𝑦 = ( 𝑥 ‘ 𝑋 ) → ( 𝑦 ∈ 𝐵 ↔ ( 𝑥 ‘ 𝑋 ) ∈ 𝐵 ) )
13		sneq	⊢ ( 𝑦 = ( 𝑥 ‘ 𝑋 ) → { 𝑦 } = { ( 𝑥 ‘ 𝑋 ) } )
14	13	xpeq2d	⊢ ( 𝑦 = ( 𝑥 ‘ 𝑋 ) → ( { 𝑋 } × { 𝑦 } ) = ( { 𝑋 } × { ( 𝑥 ‘ 𝑋 ) } ) )
15	14	eqeq2d	⊢ ( 𝑦 = ( 𝑥 ‘ 𝑋 ) → ( 𝑥 = ( { 𝑋 } × { 𝑦 } ) ↔ 𝑥 = ( { 𝑋 } × { ( 𝑥 ‘ 𝑋 ) } ) ) )
16	12 15	anbi12d	⊢ ( 𝑦 = ( 𝑥 ‘ 𝑋 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( { 𝑋 } × { 𝑦 } ) ) ↔ ( ( 𝑥 ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑥 = ( { 𝑋 } × { ( 𝑥 ‘ 𝑋 ) } ) ) ) )
17	11 16	syl5ibrcom	⊢ ( 𝑥 ∈ ( 𝐵 ↑_m { 𝑋 } ) → ( 𝑦 = ( 𝑥 ‘ 𝑋 ) → ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( { 𝑋 } × { 𝑦 } ) ) ) )
18	17	imp	⊢ ( ( 𝑥 ∈ ( 𝐵 ↑_m { 𝑋 } ) ∧ 𝑦 = ( 𝑥 ‘ 𝑋 ) ) → ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( { 𝑋 } × { 𝑦 } ) ) )
19		fconst6g	⊢ ( 𝑦 ∈ 𝐵 → ( { 𝑋 } × { 𝑦 } ) : { 𝑋 } ⟶ 𝐵 )
20		snex	⊢ { 𝑋 } ∈ V
21	2 20	elmap	⊢ ( ( { 𝑋 } × { 𝑦 } ) ∈ ( 𝐵 ↑_m { 𝑋 } ) ↔ ( { 𝑋 } × { 𝑦 } ) : { 𝑋 } ⟶ 𝐵 )
22	19 21	sylibr	⊢ ( 𝑦 ∈ 𝐵 → ( { 𝑋 } × { 𝑦 } ) ∈ ( 𝐵 ↑_m { 𝑋 } ) )
23		vex	⊢ 𝑦 ∈ V
24	23	fvconst2	⊢ ( 𝑋 ∈ { 𝑋 } → ( ( { 𝑋 } × { 𝑦 } ) ‘ 𝑋 ) = 𝑦 )
25	6 24	mp1i	⊢ ( 𝑦 ∈ 𝐵 → ( ( { 𝑋 } × { 𝑦 } ) ‘ 𝑋 ) = 𝑦 )
26	25	eqcomd	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 = ( ( { 𝑋 } × { 𝑦 } ) ‘ 𝑋 ) )
27	22 26	jca	⊢ ( 𝑦 ∈ 𝐵 → ( ( { 𝑋 } × { 𝑦 } ) ∈ ( 𝐵 ↑_m { 𝑋 } ) ∧ 𝑦 = ( ( { 𝑋 } × { 𝑦 } ) ‘ 𝑋 ) ) )
28		eleq1	⊢ ( 𝑥 = ( { 𝑋 } × { 𝑦 } ) → ( 𝑥 ∈ ( 𝐵 ↑_m { 𝑋 } ) ↔ ( { 𝑋 } × { 𝑦 } ) ∈ ( 𝐵 ↑_m { 𝑋 } ) ) )
29		fveq1	⊢ ( 𝑥 = ( { 𝑋 } × { 𝑦 } ) → ( 𝑥 ‘ 𝑋 ) = ( ( { 𝑋 } × { 𝑦 } ) ‘ 𝑋 ) )
30	29	eqeq2d	⊢ ( 𝑥 = ( { 𝑋 } × { 𝑦 } ) → ( 𝑦 = ( 𝑥 ‘ 𝑋 ) ↔ 𝑦 = ( ( { 𝑋 } × { 𝑦 } ) ‘ 𝑋 ) ) )
31	28 30	anbi12d	⊢ ( 𝑥 = ( { 𝑋 } × { 𝑦 } ) → ( ( 𝑥 ∈ ( 𝐵 ↑_m { 𝑋 } ) ∧ 𝑦 = ( 𝑥 ‘ 𝑋 ) ) ↔ ( ( { 𝑋 } × { 𝑦 } ) ∈ ( 𝐵 ↑_m { 𝑋 } ) ∧ 𝑦 = ( ( { 𝑋 } × { 𝑦 } ) ‘ 𝑋 ) ) ) )
32	27 31	syl5ibrcom	⊢ ( 𝑦 ∈ 𝐵 → ( 𝑥 = ( { 𝑋 } × { 𝑦 } ) → ( 𝑥 ∈ ( 𝐵 ↑_m { 𝑋 } ) ∧ 𝑦 = ( 𝑥 ‘ 𝑋 ) ) ) )
33	32	imp	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( { 𝑋 } × { 𝑦 } ) ) → ( 𝑥 ∈ ( 𝐵 ↑_m { 𝑋 } ) ∧ 𝑦 = ( 𝑥 ‘ 𝑋 ) ) )
34	18 33	impbii	⊢ ( ( 𝑥 ∈ ( 𝐵 ↑_m { 𝑋 } ) ∧ 𝑦 = ( 𝑥 ‘ 𝑋 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( { 𝑋 } × { 𝑦 } ) ) )
35	1	oveq2i	⊢ ( 𝐵 ↑_m 𝑆 ) = ( 𝐵 ↑_m { 𝑋 } )
36	35	eleq2i	⊢ ( 𝑥 ∈ ( 𝐵 ↑_m 𝑆 ) ↔ 𝑥 ∈ ( 𝐵 ↑_m { 𝑋 } ) )
37	36	anbi1i	⊢ ( ( 𝑥 ∈ ( 𝐵 ↑_m 𝑆 ) ∧ 𝑦 = ( 𝑥 ‘ 𝑋 ) ) ↔ ( 𝑥 ∈ ( 𝐵 ↑_m { 𝑋 } ) ∧ 𝑦 = ( 𝑥 ‘ 𝑋 ) ) )
38	1	xpeq1i	⊢ ( 𝑆 × { 𝑦 } ) = ( { 𝑋 } × { 𝑦 } )
39	38	eqeq2i	⊢ ( 𝑥 = ( 𝑆 × { 𝑦 } ) ↔ 𝑥 = ( { 𝑋 } × { 𝑦 } ) )
40	39	anbi2i	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( 𝑆 × { 𝑦 } ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( { 𝑋 } × { 𝑦 } ) ) )
41	34 37 40	3bitr4i	⊢ ( ( 𝑥 ∈ ( 𝐵 ↑_m 𝑆 ) ∧ 𝑦 = ( 𝑥 ‘ 𝑋 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( 𝑆 × { 𝑦 } ) ) )
42	41	opabbii	⊢ { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ ( 𝐵 ↑_m 𝑆 ) ∧ 𝑦 = ( 𝑥 ‘ 𝑋 ) ) } = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( 𝑆 × { 𝑦 } ) ) }
43		df-mpt	⊢ ( 𝑥 ∈ ( 𝐵 ↑_m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐵 ↑_m 𝑆 ) ∧ 𝑦 = ( 𝑥 ‘ 𝑋 ) ) }
44	4 43	eqtri	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐵 ↑_m 𝑆 ) ∧ 𝑦 = ( 𝑥 ‘ 𝑋 ) ) }
45	44	cnveqi	⊢ ^◡ 𝐹 = ^◡ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐵 ↑_m 𝑆 ) ∧ 𝑦 = ( 𝑥 ‘ 𝑋 ) ) }
46		cnvopab	⊢ ^◡ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐵 ↑_m 𝑆 ) ∧ 𝑦 = ( 𝑥 ‘ 𝑋 ) ) } = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ ( 𝐵 ↑_m 𝑆 ) ∧ 𝑦 = ( 𝑥 ‘ 𝑋 ) ) }
47	45 46	eqtri	⊢ ^◡ 𝐹 = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ ( 𝐵 ↑_m 𝑆 ) ∧ 𝑦 = ( 𝑥 ‘ 𝑋 ) ) }
48		df-mpt	⊢ ( 𝑦 ∈ 𝐵 ↦ ( 𝑆 × { 𝑦 } ) ) = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( 𝑆 × { 𝑦 } ) ) }
49	42 47 48	3eqtr4i	⊢ ^◡ 𝐹 = ( 𝑦 ∈ 𝐵 ↦ ( 𝑆 × { 𝑦 } ) )

Metamath Proof Explorer

Theorem mapsncnv

Proof