Theorem ssmapsn 45158

Description: A subset 𝐶 of a set exponentiation to a singleton, is its projection 𝐷 exponentiated to the singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

Hypotheses

Ref	Expression
ssmapsn.f	⊢ Ⅎ𝑓𝐷
ssmapsn.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
ssmapsn.c	⊢ (𝜑 → 𝐶 ⊆ (𝐵 ↑m {𝐴}))
ssmapsn.d	⊢ 𝐷 = ∪ 𝑓 ∈ 𝐶 ran 𝑓

Assertion

Ref	Expression
ssmapsn	⊢ (𝜑 → 𝐶 = (𝐷 ↑m {𝐴}))

Distinct variable groups:   𝐴,𝑓   𝐶,𝑓   𝜑,𝑓

Allowed substitution hints:   𝐵(𝑓)   𝐷(𝑓)   𝑉(𝑓)

Proof of Theorem ssmapsn

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssmapsn.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ⊆ (𝐵 ↑m {𝐴}))
2	1	sselda 3994	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → 𝑓 ∈ (𝐵 ↑m {𝐴}))
3		elmapi 8887	. . . . . . 7 ⊢ (𝑓 ∈ (𝐵 ↑m {𝐴}) → 𝑓:{𝐴}⟶𝐵)
4	2, 3	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → 𝑓:{𝐴}⟶𝐵)
5	4	ffnd 6737	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → 𝑓 Fn {𝐴})
6		ssmapsn.d	. . . . . . . 8 ⊢ 𝐷 = ∪ 𝑓 ∈ 𝐶 ran 𝑓
7	6	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐷 = ∪ 𝑓 ∈ 𝐶 ran 𝑓)
8		ovexd 7465	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ↑m {𝐴}) ∈ V)
9	8, 1	ssexd 5329	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ V)
10		rnexg 7924	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝐶 → ran 𝑓 ∈ V)
11	10	rgen 3060	. . . . . . . 8 ⊢ ∀𝑓 ∈ 𝐶 ran 𝑓 ∈ V
12		iunexg 7986	. . . . . . . 8 ⊢ ((𝐶 ∈ V ∧ ∀𝑓 ∈ 𝐶 ran 𝑓 ∈ V) → ∪ 𝑓 ∈ 𝐶 ran 𝑓 ∈ V)
13	9, 11, 12	sylancl 586	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑓 ∈ 𝐶 ran 𝑓 ∈ V)
14	7, 13	eqeltrd 2838	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ V)
15	14	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → 𝐷 ∈ V)
16		ssiun2 5051	. . . . . . . 8 ⊢ (𝑓 ∈ 𝐶 → ran 𝑓 ⊆ ∪ 𝑓 ∈ 𝐶 ran 𝑓)
17	16	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → ran 𝑓 ⊆ ∪ 𝑓 ∈ 𝐶 ran 𝑓)
18		ssmapsn.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
19		snidg 4664	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})
20	18, 19	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
21	20	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → 𝐴 ∈ {𝐴})
22	5, 21	fnfvelrnd 7101	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → (𝑓‘𝐴) ∈ ran 𝑓)
23	17, 22	sseldd 3995	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → (𝑓‘𝐴) ∈ ∪ 𝑓 ∈ 𝐶 ran 𝑓)
24	23, 6	eleqtrrdi 2849	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → (𝑓‘𝐴) ∈ 𝐷)
25	5, 15, 24	elmapsnd 45146	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → 𝑓 ∈ (𝐷 ↑m {𝐴}))
26	14	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) → 𝐷 ∈ V)
27		snex 5441	. . . . . . . . 9 ⊢ {𝐴} ∈ V
28	27	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) → {𝐴} ∈ V)
29		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) → 𝑓 ∈ (𝐷 ↑m {𝐴}))
30	20	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) → 𝐴 ∈ {𝐴})
31	26, 28, 29, 30	fvmap 45140	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) → (𝑓‘𝐴) ∈ 𝐷)
32		rneq 5949	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → ran 𝑓 = ran 𝑔)
33	32	cbviunv 5044	. . . . . . . 8 ⊢ ∪ 𝑓 ∈ 𝐶 ran 𝑓 = ∪ 𝑔 ∈ 𝐶 ran 𝑔
34	6, 33	eqtri 2762	. . . . . . 7 ⊢ 𝐷 = ∪ 𝑔 ∈ 𝐶 ran 𝑔
35	31, 34	eleqtrdi 2848	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) → (𝑓‘𝐴) ∈ ∪ 𝑔 ∈ 𝐶 ran 𝑔)
36		eliun 4999	. . . . . 6 ⊢ ((𝑓‘𝐴) ∈ ∪ 𝑔 ∈ 𝐶 ran 𝑔 ↔ ∃𝑔 ∈ 𝐶 (𝑓‘𝐴) ∈ ran 𝑔)
37	35, 36	sylib 218	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) → ∃𝑔 ∈ 𝐶 (𝑓‘𝐴) ∈ ran 𝑔)
38		simp3 1137	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → (𝑓‘𝐴) ∈ ran 𝑔)
39		simp1l 1196	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝜑)
40	39, 18	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝐴 ∈ 𝑉)
41		eqid 2734	. . . . . . . . 9 ⊢ {𝐴} = {𝐴}
42		simp1r 1197	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝑓 ∈ (𝐷 ↑m {𝐴}))
43		elmapfn 8903	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝐷 ↑m {𝐴}) → 𝑓 Fn {𝐴})
44	42, 43	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝑓 Fn {𝐴})
45	1	sselda 3994	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → 𝑔 ∈ (𝐵 ↑m {𝐴}))
46		elmapfn 8903	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ (𝐵 ↑m {𝐴}) → 𝑔 Fn {𝐴})
47	45, 46	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶) → 𝑔 Fn {𝐴})
48	47	3adant3 1131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝑔 Fn {𝐴})
49	48	3adant1r 1176	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝑔 Fn {𝐴})
50	40, 41, 44, 49	fsneqrn 45153	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → (𝑓 = 𝑔 ↔ (𝑓‘𝐴) ∈ ran 𝑔))
51	38, 50	mpbird 257	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝑓 = 𝑔)
52		simp2 1136	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝑔 ∈ 𝐶)
53	51, 52	eqeltrd 2838	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) ∧ 𝑔 ∈ 𝐶 ∧ (𝑓‘𝐴) ∈ ran 𝑔) → 𝑓 ∈ 𝐶)
54	53	rexlimdv3a 3156	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) → (∃𝑔 ∈ 𝐶 (𝑓‘𝐴) ∈ ran 𝑔 → 𝑓 ∈ 𝐶))
55	37, 54	mpd 15	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐷 ↑m {𝐴})) → 𝑓 ∈ 𝐶)
56	25, 55	impbida 801	. . 3 ⊢ (𝜑 → (𝑓 ∈ 𝐶 ↔ 𝑓 ∈ (𝐷 ↑m {𝐴})))
57	56	alrimiv 1924	. 2 ⊢ (𝜑 → ∀𝑓(𝑓 ∈ 𝐶 ↔ 𝑓 ∈ (𝐷 ↑m {𝐴})))
58		nfcv 2902	. . 3 ⊢ Ⅎ𝑓𝐶
59		ssmapsn.f	. . . 4 ⊢ Ⅎ𝑓𝐷
60		nfcv 2902	. . . 4 ⊢ Ⅎ𝑓 ↑m
61		nfcv 2902	. . . 4 ⊢ Ⅎ𝑓{𝐴}
62	59, 60, 61	nfov 7460	. . 3 ⊢ Ⅎ𝑓(𝐷 ↑m {𝐴})
63	58, 62	cleqf 2931	. 2 ⊢ (𝐶 = (𝐷 ↑m {𝐴}) ↔ ∀𝑓(𝑓 ∈ 𝐶 ↔ 𝑓 ∈ (𝐷 ↑m {𝐴})))
64	57, 63	sylibr 234	1 ⊢ (𝜑 → 𝐶 = (𝐷 ↑m {𝐴}))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086  ∀wal 1534   = wceq 1536   ∈ wcel 2105  Ⅎwnfc 2887  ∀wral 3058  ∃wrex 3067  Vcvv 3477   ⊆ wss 3962  {csn 4630  ∪ ciun 4995  ran crn 5689   Fn wfn 6557  ⟶wf 6558  ‘cfv 6562  (class class class)co 7430   ↑_m cmap 8864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8012  df-2nd 8013  df-map 8866

This theorem is referenced by:  vonvolmbllem  46615  vonvolmbl2  46618  vonvol2  46619