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	$⊢ F defAt A \to (F'''' A) \in ran F$

Proof

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

Metamath Proof Explorer

Theorem funressndmafv2rn

Proof