Theorem funressndmafv2rn

Description: The alternate function value at a class A is defined, i.e., in the range of the function if the function is defined at A . (Contributed by AV, 2-Sep-2022)

	Ref	Expression
Assertion	funressndmafv2rn	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		dfatafv2iota	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = ( ℩ 𝑦 𝐴 𝐹 𝑦 ) )
2		df-dfat	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
3		sneq	⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
4	3	reseq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐹 ↾ { 𝑥 } ) = ( 𝐹 ↾ { 𝐴 } ) )
5	4	funeqd	⊢ ( 𝑥 = 𝐴 → ( Fun ( 𝐹 ↾ { 𝑥 } ) ↔ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
6		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ dom 𝐹 ↔ 𝐴 ∈ dom 𝐹 ) )
7	5 6	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( Fun ( 𝐹 ↾ { 𝑥 } ) ∧ 𝑥 ∈ dom 𝐹 ) ↔ ( Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 ∈ dom 𝐹 ) ) )
8		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 𝑦 ↔ 𝐴 𝐹 𝑦 ) )
9	8	iotabidv	⊢ ( 𝑥 = 𝐴 → ( ℩ 𝑦 𝑥 𝐹 𝑦 ) = ( ℩ 𝑦 𝐴 𝐹 𝑦 ) )
10	9	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ∈ ran 𝐹 ↔ ( ℩ 𝑦 𝐴 𝐹 𝑦 ) ∈ ran 𝐹 ) )
11	7 10	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( Fun ( 𝐹 ↾ { 𝑥 } ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ∈ ran 𝐹 ) ↔ ( ( Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 ∈ dom 𝐹 ) → ( ℩ 𝑦 𝐴 𝐹 𝑦 ) ∈ ran 𝐹 ) ) )
12		eqid	⊢ ( ℩ 𝑦 𝑥 𝐹 𝑦 ) = ( ℩ 𝑦 𝑥 𝐹 𝑦 )
13		iotaex	⊢ ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ∈ V
14		eqeq2	⊢ ( 𝑧 = ( ℩ 𝑦 𝑥 𝐹 𝑦 ) → ( ( ℩ 𝑦 𝑥 𝐹 𝑦 ) = 𝑧 ↔ ( ℩ 𝑦 𝑥 𝐹 𝑦 ) = ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ) )
15		breq2	⊢ ( 𝑧 = ( ℩ 𝑦 𝑥 𝐹 𝑦 ) → ( 𝑥 𝐹 𝑧 ↔ 𝑥 𝐹 ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ) )
16	14 15	bibi12d	⊢ ( 𝑧 = ( ℩ 𝑦 𝑥 𝐹 𝑦 ) → ( ( ( ℩ 𝑦 𝑥 𝐹 𝑦 ) = 𝑧 ↔ 𝑥 𝐹 𝑧 ) ↔ ( ( ℩ 𝑦 𝑥 𝐹 𝑦 ) = ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ↔ 𝑥 𝐹 ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ) ) )
17	16	imbi2d	⊢ ( 𝑧 = ( ℩ 𝑦 𝑥 𝐹 𝑦 ) → ( ( ( Fun ( 𝐹 ↾ { 𝑥 } ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ℩ 𝑦 𝑥 𝐹 𝑦 ) = 𝑧 ↔ 𝑥 𝐹 𝑧 ) ) ↔ ( ( Fun ( 𝐹 ↾ { 𝑥 } ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ℩ 𝑦 𝑥 𝐹 𝑦 ) = ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ↔ 𝑥 𝐹 ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ) ) ) )
18		eldmg	⊢ ( 𝑥 ∈ dom 𝐹 → ( 𝑥 ∈ dom 𝐹 ↔ ∃ 𝑧 𝑥 𝐹 𝑧 ) )
19	18	ibi	⊢ ( 𝑥 ∈ dom 𝐹 → ∃ 𝑧 𝑥 𝐹 𝑧 )
20	19	adantl	⊢ ( ( Fun ( 𝐹 ↾ { 𝑥 } ) ∧ 𝑥 ∈ dom 𝐹 ) → ∃ 𝑧 𝑥 𝐹 𝑧 )
21		funressnvmo	⊢ ( Fun ( 𝐹 ↾ { 𝑥 } ) → ∃* 𝑧 𝑥 𝐹 𝑧 )
22	21	adantr	⊢ ( ( Fun ( 𝐹 ↾ { 𝑥 } ) ∧ 𝑥 ∈ dom 𝐹 ) → ∃* 𝑧 𝑥 𝐹 𝑧 )
23		moeu	⊢ ( ∃* 𝑧 𝑥 𝐹 𝑧 ↔ ( ∃ 𝑧 𝑥 𝐹 𝑧 → ∃! 𝑧 𝑥 𝐹 𝑧 ) )
24	22 23	sylib	⊢ ( ( Fun ( 𝐹 ↾ { 𝑥 } ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ∃ 𝑧 𝑥 𝐹 𝑧 → ∃! 𝑧 𝑥 𝐹 𝑧 ) )
25	20 24	mpd	⊢ ( ( Fun ( 𝐹 ↾ { 𝑥 } ) ∧ 𝑥 ∈ dom 𝐹 ) → ∃! 𝑧 𝑥 𝐹 𝑧 )
26		iota1	⊢ ( ∃! 𝑧 𝑥 𝐹 𝑧 → ( 𝑥 𝐹 𝑧 ↔ ( ℩ 𝑧 𝑥 𝐹 𝑧 ) = 𝑧 ) )
27		breq2	⊢ ( 𝑧 = 𝑦 → ( 𝑥 𝐹 𝑧 ↔ 𝑥 𝐹 𝑦 ) )
28	27	cbviotavw	⊢ ( ℩ 𝑧 𝑥 𝐹 𝑧 ) = ( ℩ 𝑦 𝑥 𝐹 𝑦 )
29	28	eqeq1i	⊢ ( ( ℩ 𝑧 𝑥 𝐹 𝑧 ) = 𝑧 ↔ ( ℩ 𝑦 𝑥 𝐹 𝑦 ) = 𝑧 )
30	26 29	bitr2di	⊢ ( ∃! 𝑧 𝑥 𝐹 𝑧 → ( ( ℩ 𝑦 𝑥 𝐹 𝑦 ) = 𝑧 ↔ 𝑥 𝐹 𝑧 ) )
31	25 30	syl	⊢ ( ( Fun ( 𝐹 ↾ { 𝑥 } ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ℩ 𝑦 𝑥 𝐹 𝑦 ) = 𝑧 ↔ 𝑥 𝐹 𝑧 ) )
32	13 17 31	vtocl	⊢ ( ( Fun ( 𝐹 ↾ { 𝑥 } ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ℩ 𝑦 𝑥 𝐹 𝑦 ) = ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ↔ 𝑥 𝐹 ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ) )
33	12 32	mpbii	⊢ ( ( Fun ( 𝐹 ↾ { 𝑥 } ) ∧ 𝑥 ∈ dom 𝐹 ) → 𝑥 𝐹 ( ℩ 𝑦 𝑥 𝐹 𝑦 ) )
34		df-br	⊢ ( 𝑥 𝐹 ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ↔ ⟨ 𝑥 , ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ⟩ ∈ 𝐹 )
35	33 34	sylib	⊢ ( ( Fun ( 𝐹 ↾ { 𝑥 } ) ∧ 𝑥 ∈ dom 𝐹 ) → ⟨ 𝑥 , ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ⟩ ∈ 𝐹 )
36		vex	⊢ 𝑥 ∈ V
37		opeq1	⊢ ( 𝑧 = 𝑥 → ⟨ 𝑧 , ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ⟩ = ⟨ 𝑥 , ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ⟩ )
38	37	eleq1d	⊢ ( 𝑧 = 𝑥 → ( ⟨ 𝑧 , ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ⟩ ∈ 𝐹 ↔ ⟨ 𝑥 , ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ⟩ ∈ 𝐹 ) )
39	36 38	spcev	⊢ ( ⟨ 𝑥 , ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ⟩ ∈ 𝐹 → ∃ 𝑧 ⟨ 𝑧 , ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ⟩ ∈ 𝐹 )
40	35 39	syl	⊢ ( ( Fun ( 𝐹 ↾ { 𝑥 } ) ∧ 𝑥 ∈ dom 𝐹 ) → ∃ 𝑧 ⟨ 𝑧 , ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ⟩ ∈ 𝐹 )
41	13	elrn2	⊢ ( ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ∈ ran 𝐹 ↔ ∃ 𝑧 ⟨ 𝑧 , ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ⟩ ∈ 𝐹 )
42	40 41	sylibr	⊢ ( ( Fun ( 𝐹 ↾ { 𝑥 } ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ℩ 𝑦 𝑥 𝐹 𝑦 ) ∈ ran 𝐹 )
43	11 42	vtoclg	⊢ ( 𝐴 ∈ dom 𝐹 → ( ( Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 ∈ dom 𝐹 ) → ( ℩ 𝑦 𝐴 𝐹 𝑦 ) ∈ ran 𝐹 ) )
44	43	anabsi6	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( ℩ 𝑦 𝐴 𝐹 𝑦 ) ∈ ran 𝐹 )
45	2 44	sylbi	⊢ ( 𝐹 defAt 𝐴 → ( ℩ 𝑦 𝐴 𝐹 𝑦 ) ∈ ran 𝐹 )
46	1 45	eqeltrd	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 )