Theorem mapsncnv 6943

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.)

Hypotheses

Ref	Expression
mapsncnv.s	⊢ 𝑆 = {𝑋}
mapsncnv.b	⊢ 𝐵 ∈ V
mapsncnv.x	⊢ 𝑋 ∈ V
mapsncnv.f	⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↦ (𝑥‘𝑋))

Assertion

Ref	Expression
mapsncnv	⊢ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦}))

Distinct variable groups:   𝑥,𝐵,𝑦   𝑥,𝑆,𝑦   𝑦,𝑋

Allowed substitution hints:   𝐹(𝑥,𝑦)   𝑋(𝑥)

Proof of Theorem mapsncnv

Step	Hyp	Ref	Expression
1		elmapi 6917	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) → 𝑥:{𝑋}⟶𝐵)
2		mapsncnv.x	. . . . . . . . . 10 ⊢ 𝑋 ∈ V
3	2	snid 3725	. . . . . . . . 9 ⊢ 𝑋 ∈ {𝑋}
4		ffvelcdm 5815	. . . . . . . . 9 ⊢ ((𝑥:{𝑋}⟶𝐵 ∧ 𝑋 ∈ {𝑋}) → (𝑥‘𝑋) ∈ 𝐵)
5	1, 3, 4	sylancl 413	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) → (𝑥‘𝑋) ∈ 𝐵)
6		eqid 2234	. . . . . . . . 9 ⊢ {𝑋} = {𝑋}
7		mapsncnv.b	. . . . . . . . 9 ⊢ 𝐵 ∈ V
8	6, 7, 2	mapsnconst 6942	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) → 𝑥 = ({𝑋} × {(𝑥‘𝑋)}))
9	5, 8	jca 306	. . . . . . 7 ⊢ (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) → ((𝑥‘𝑋) ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {(𝑥‘𝑋)})))
10		eleq1 2297	. . . . . . . 8 ⊢ (𝑦 = (𝑥‘𝑋) → (𝑦 ∈ 𝐵 ↔ (𝑥‘𝑋) ∈ 𝐵))
11		sneq 3705	. . . . . . . . . 10 ⊢ (𝑦 = (𝑥‘𝑋) → {𝑦} = {(𝑥‘𝑋)})
12	11	xpeq2d 4778	. . . . . . . . 9 ⊢ (𝑦 = (𝑥‘𝑋) → ({𝑋} × {𝑦}) = ({𝑋} × {(𝑥‘𝑋)}))
13	12	eqeq2d 2246	. . . . . . . 8 ⊢ (𝑦 = (𝑥‘𝑋) → (𝑥 = ({𝑋} × {𝑦}) ↔ 𝑥 = ({𝑋} × {(𝑥‘𝑋)})))
14	10, 13	anbi12d 473	. . . . . . 7 ⊢ (𝑦 = (𝑥‘𝑋) → ((𝑦 ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {𝑦})) ↔ ((𝑥‘𝑋) ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {(𝑥‘𝑋)}))))
15	9, 14	syl5ibrcom 157	. . . . . 6 ⊢ (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) → (𝑦 = (𝑥‘𝑋) → (𝑦 ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {𝑦}))))
16	15	imp 124	. . . . 5 ⊢ ((𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (𝑥‘𝑋)) → (𝑦 ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {𝑦})))
17		fconst6g 5571	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝐵 → ({𝑋} × {𝑦}):{𝑋}⟶𝐵)
18	2	snex 4303	. . . . . . . . . 10 ⊢ {𝑋} ∈ V
19	7, 18	elmap 6924	. . . . . . . . 9 ⊢ (({𝑋} × {𝑦}) ∈ (𝐵 ↑𝑚 {𝑋}) ↔ ({𝑋} × {𝑦}):{𝑋}⟶𝐵)
20	17, 19	sylibr 134	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐵 → ({𝑋} × {𝑦}) ∈ (𝐵 ↑𝑚 {𝑋}))
21		vex 2818	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
22	21	fvconst2 5905	. . . . . . . . . 10 ⊢ (𝑋 ∈ {𝑋} → (({𝑋} × {𝑦})‘𝑋) = 𝑦)
23	3, 22	mp1i 10	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝐵 → (({𝑋} × {𝑦})‘𝑋) = 𝑦)
24	23	eqcomd 2240	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐵 → 𝑦 = (({𝑋} × {𝑦})‘𝑋))
25	20, 24	jca 306	. . . . . . 7 ⊢ (𝑦 ∈ 𝐵 → (({𝑋} × {𝑦}) ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (({𝑋} × {𝑦})‘𝑋)))
26		eleq1 2297	. . . . . . . 8 ⊢ (𝑥 = ({𝑋} × {𝑦}) → (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) ↔ ({𝑋} × {𝑦}) ∈ (𝐵 ↑𝑚 {𝑋})))
27		fveq1 5674	. . . . . . . . 9 ⊢ (𝑥 = ({𝑋} × {𝑦}) → (𝑥‘𝑋) = (({𝑋} × {𝑦})‘𝑋))
28	27	eqeq2d 2246	. . . . . . . 8 ⊢ (𝑥 = ({𝑋} × {𝑦}) → (𝑦 = (𝑥‘𝑋) ↔ 𝑦 = (({𝑋} × {𝑦})‘𝑋)))
29	26, 28	anbi12d 473	. . . . . . 7 ⊢ (𝑥 = ({𝑋} × {𝑦}) → ((𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (𝑥‘𝑋)) ↔ (({𝑋} × {𝑦}) ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (({𝑋} × {𝑦})‘𝑋))))
30	25, 29	syl5ibrcom 157	. . . . . 6 ⊢ (𝑦 ∈ 𝐵 → (𝑥 = ({𝑋} × {𝑦}) → (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (𝑥‘𝑋))))
31	30	imp 124	. . . . 5 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {𝑦})) → (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (𝑥‘𝑋)))
32	16, 31	impbii 126	. . . 4 ⊢ ((𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (𝑥‘𝑋)) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {𝑦})))
33		mapsncnv.s	. . . . . . 7 ⊢ 𝑆 = {𝑋}
34	33	oveq2i 6069	. . . . . 6 ⊢ (𝐵 ↑𝑚 𝑆) = (𝐵 ↑𝑚 {𝑋})
35	34	eleq2i 2301	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↔ 𝑥 ∈ (𝐵 ↑𝑚 {𝑋}))
36	35	anbi1i 458	. . . 4 ⊢ ((𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋)) ↔ (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (𝑥‘𝑋)))
37	33	xpeq1i 4774	. . . . . 6 ⊢ (𝑆 × {𝑦}) = ({𝑋} × {𝑦})
38	37	eqeq2i 2245	. . . . 5 ⊢ (𝑥 = (𝑆 × {𝑦}) ↔ 𝑥 = ({𝑋} × {𝑦}))
39	38	anbi2i 457	. . . 4 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (𝑆 × {𝑦})) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {𝑦})))
40	32, 36, 39	3bitr4i 212	. . 3 ⊢ ((𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋)) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = (𝑆 × {𝑦})))
41	40	opabbii 4182	. 2 ⊢ {⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋))} = {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐵 ∧ 𝑥 = (𝑆 × {𝑦}))}
42		mapsncnv.f	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↦ (𝑥‘𝑋))
43		df-mpt 4178	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↦ (𝑥‘𝑋)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋))}
44	42, 43	eqtri 2255	. . . 4 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋))}
45	44	cnveqi 4935	. . 3 ⊢ ◡𝐹 = ◡{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋))}
46		cnvopab 5169	. . 3 ⊢ ◡{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋))} = {⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋))}
47	45, 46	eqtri 2255	. 2 ⊢ ◡𝐹 = {⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋))}
48		df-mpt 4178	. 2 ⊢ (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦})) = {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐵 ∧ 𝑥 = (𝑆 × {𝑦}))}
49	41, 47, 48	3eqtr4i 2265	1 ⊢ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦}))

Syntax hints:   ∧ wa 104   = wceq 1398   ∈ wcel 2205  Vcvv 2815  {csn 3694  {copab 4175   ↦ cmpt 4176   × cxp 4752  ^◡ccnv 4753  ⟶wf 5353  ‘cfv 5357  (class class class)co 6058   ↑_𝑚 cmap 6895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327  ax-un 4559  ax-setind 4664

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-ral 2527  df-rex 2528  df-reu 2529  df-v 2817  df-sbc 3046  df-dif 3216  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-opab 4177  df-mpt 4178  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-rn 4765  df-res 4766  df-ima 4767  df-iota 5317  df-fun 5359  df-fn 5360  df-f 5361  df-f1 5362  df-fo 5363  df-f1o 5364  df-fv 5365  df-ov 6061  df-oprab 6062  df-mpo 6063  df-map 6897

This theorem is referenced by:  mapsnf1o2  6944  mapsnf1o3  6945