Theorem fvimacnv

Description: The argument of a function value belongs to the preimage of any class containing the function value. Raph Levien remarks: "This proof is unsatisfying, because it seems to me that funimass2 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006)

	Ref	Expression
Assertion	fvimacnv	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to \left(F\left(A\right)\in B\leftrightarrow A\in F^{-1}\left[B\right]\right)$$

Proof

Step	Hyp	Ref	Expression
1		funfvop	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to ⟨A,F\left(A\right)⟩\in F$$
2		fvex	$$⊢F\left(A\right)\in \mathrm{V}$$
3		opelcnvg	$$⊢\left(F\left(A\right)\in \mathrm{V}\wedge A\in \mathrm{dom}F\right)\to \left(⟨F\left(A\right),A⟩\in F^{-1}\leftrightarrow ⟨A,F\left(A\right)⟩\in F\right)$$
4	2 3	mpan	$$⊢A\in \mathrm{dom}F\to \left(⟨F\left(A\right),A⟩\in F^{-1}\leftrightarrow ⟨A,F\left(A\right)⟩\in F\right)$$
5	4	adantl	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to \left(⟨F\left(A\right),A⟩\in F^{-1}\leftrightarrow ⟨A,F\left(A\right)⟩\in F\right)$$
6	1 5	mpbird	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to ⟨F\left(A\right),A⟩\in F^{-1}$$
7		elimasng	$$⊢\left(F\left(A\right)\in \mathrm{V}\wedge A\in \mathrm{dom}F\right)\to \left(A\in F^{-1}\left[\left\{F\left(A\right)\right\}\right]\leftrightarrow ⟨F\left(A\right),A⟩\in F^{-1}\right)$$
8	2 7	mpan	$$⊢A\in \mathrm{dom}F\to \left(A\in F^{-1}\left[\left\{F\left(A\right)\right\}\right]\leftrightarrow ⟨F\left(A\right),A⟩\in F^{-1}\right)$$
9	8	adantl	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to \left(A\in F^{-1}\left[\left\{F\left(A\right)\right\}\right]\leftrightarrow ⟨F\left(A\right),A⟩\in F^{-1}\right)$$
10	6 9	mpbird	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to A\in F^{-1}\left[\left\{F\left(A\right)\right\}\right]$$
11	2	snss	$$⊢F\left(A\right)\in B\leftrightarrow \left\{F\left(A\right)\right\}\subseteq B$$
12		imass2	$$⊢\left\{F\left(A\right)\right\}\subseteq B\to F^{-1}\left[\left\{F\left(A\right)\right\}\right]\subseteq F^{-1}\left[B\right]$$
13	11 12	sylbi	$$⊢F\left(A\right)\in B\to F^{-1}\left[\left\{F\left(A\right)\right\}\right]\subseteq F^{-1}\left[B\right]$$
14	13	sseld	$$⊢F\left(A\right)\in B\to \left(A\in F^{-1}\left[\left\{F\left(A\right)\right\}\right]\to A\in F^{-1}\left[B\right]\right)$$
15	10 14	syl5com	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to \left(F\left(A\right)\in B\to A\in F^{-1}\left[B\right]\right)$$
16		fvimacnvi	$$⊢\left(\mathrm{Fun}F\wedge A\in F^{-1}\left[B\right]\right)\to F\left(A\right)\in B$$
17	16	ex	$$⊢\mathrm{Fun}F\to \left(A\in F^{-1}\left[B\right]\to F\left(A\right)\in B\right)$$
18	17	adantr	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to \left(A\in F^{-1}\left[B\right]\to F\left(A\right)\in B\right)$$
19	15 18	impbid	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to \left(F\left(A\right)\in B\leftrightarrow A\in F^{-1}\left[B\right]\right)$$