Theorem slotresfo 48929

Description: The condition of a structure component extractor restricted to a class being a surjection. This combined with fonex 48897 can be used to prove a class being proper. (Contributed by Zhi Wang, 20-Oct-2025.)

Hypotheses

Ref	Expression
slotresfo.e	⊢ 𝐸 Fn V
slotresfo.v	⊢ (𝑘 ∈ 𝐴 → (𝐸‘𝑘) ∈ 𝑉)
slotresfo.k	⊢ (𝑏 ∈ 𝑉 → 𝐾 ∈ 𝐴)
slotresfo.b	⊢ (𝑏 ∈ 𝑉 → 𝑏 = (𝐸‘𝐾))

Assertion

Ref	Expression
slotresfo	⊢ (𝐸 ↾ 𝐴):𝐴–onto→𝑉

Distinct variable groups:   𝐴,𝑏,𝑘   𝐸,𝑏,𝑘   𝑘,𝐾   𝑉,𝑏,𝑘

Allowed substitution hint:   𝐾(𝑏)

Proof of Theorem slotresfo

Step	Hyp	Ref	Expression
1		slotresfo.e	. . . 4 ⊢ 𝐸 Fn V
2		ssv 3959	. . . 4 ⊢ 𝐴 ⊆ V
3		fnssres 6604	. . . 4 ⊢ ((𝐸 Fn V ∧ 𝐴 ⊆ V) → (𝐸 ↾ 𝐴) Fn 𝐴)
4	1, 2, 3	mp2an 692	. . 3 ⊢ (𝐸 ↾ 𝐴) Fn 𝐴
5		fvres 6841	. . . . . 6 ⊢ (𝑘 ∈ 𝐴 → ((𝐸 ↾ 𝐴)‘𝑘) = (𝐸‘𝑘))
6		slotresfo.v	. . . . . 6 ⊢ (𝑘 ∈ 𝐴 → (𝐸‘𝑘) ∈ 𝑉)
7	5, 6	eqeltrd 2831	. . . . 5 ⊢ (𝑘 ∈ 𝐴 → ((𝐸 ↾ 𝐴)‘𝑘) ∈ 𝑉)
8	7	rgen 3049	. . . 4 ⊢ ∀𝑘 ∈ 𝐴 ((𝐸 ↾ 𝐴)‘𝑘) ∈ 𝑉
9		fnfvrnss 7054	. . . 4 ⊢ (((𝐸 ↾ 𝐴) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 ((𝐸 ↾ 𝐴)‘𝑘) ∈ 𝑉) → ran (𝐸 ↾ 𝐴) ⊆ 𝑉)
10	4, 8, 9	mp2an 692	. . 3 ⊢ ran (𝐸 ↾ 𝐴) ⊆ 𝑉
11		df-f 6485	. . 3 ⊢ ((𝐸 ↾ 𝐴):𝐴⟶𝑉 ↔ ((𝐸 ↾ 𝐴) Fn 𝐴 ∧ ran (𝐸 ↾ 𝐴) ⊆ 𝑉))
12	4, 10, 11	mpbir2an 711	. 2 ⊢ (𝐸 ↾ 𝐴):𝐴⟶𝑉
13		fveq2 6822	. . . . . 6 ⊢ (𝑘 = 𝐾 → (𝐸‘𝑘) = (𝐸‘𝐾))
14	13	eqeq2d 2742	. . . . 5 ⊢ (𝑘 = 𝐾 → (𝑏 = (𝐸‘𝑘) ↔ 𝑏 = (𝐸‘𝐾)))
15		slotresfo.k	. . . . 5 ⊢ (𝑏 ∈ 𝑉 → 𝐾 ∈ 𝐴)
16		slotresfo.b	. . . . 5 ⊢ (𝑏 ∈ 𝑉 → 𝑏 = (𝐸‘𝐾))
17	14, 15, 16	rspcedvdw 3580	. . . 4 ⊢ (𝑏 ∈ 𝑉 → ∃𝑘 ∈ 𝐴 𝑏 = (𝐸‘𝑘))
18	5	eqeq2d 2742	. . . . 5 ⊢ (𝑘 ∈ 𝐴 → (𝑏 = ((𝐸 ↾ 𝐴)‘𝑘) ↔ 𝑏 = (𝐸‘𝑘)))
19	18	rexbiia 3077	. . . 4 ⊢ (∃𝑘 ∈ 𝐴 𝑏 = ((𝐸 ↾ 𝐴)‘𝑘) ↔ ∃𝑘 ∈ 𝐴 𝑏 = (𝐸‘𝑘))
20	17, 19	sylibr 234	. . 3 ⊢ (𝑏 ∈ 𝑉 → ∃𝑘 ∈ 𝐴 𝑏 = ((𝐸 ↾ 𝐴)‘𝑘))
21	20	rgen 3049	. 2 ⊢ ∀𝑏 ∈ 𝑉 ∃𝑘 ∈ 𝐴 𝑏 = ((𝐸 ↾ 𝐴)‘𝑘)
22		dffo3 7035	. 2 ⊢ ((𝐸 ↾ 𝐴):𝐴–onto→𝑉 ↔ ((𝐸 ↾ 𝐴):𝐴⟶𝑉 ∧ ∀𝑏 ∈ 𝑉 ∃𝑘 ∈ 𝐴 𝑏 = ((𝐸 ↾ 𝐴)‘𝑘)))
23	12, 21, 22	mpbir2an 711	1 ⊢ (𝐸 ↾ 𝐴):𝐴–onto→𝑉

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056  Vcvv 3436   ⊆ wss 3902  ran crn 5617   ↾ cres 5618   Fn wfn 6476  ⟶wf 6477  –onto→wfo 6479  ‘cfv 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fo 6487  df-fv 6489

This theorem is referenced by:  basresprsfo  49009  basrestermcfo  49606