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	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		funfvop	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 )
2		fvex	⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
3		opelcnvg	⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ V ∧ 𝐴 ∈ dom 𝐹 ) → ( ⟨ ( 𝐹 ‘ 𝐴 ) , 𝐴 ⟩ ∈ ◡ 𝐹 ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 ) )
4	2 3	mpan	⊢ ( 𝐴 ∈ dom 𝐹 → ( ⟨ ( 𝐹 ‘ 𝐴 ) , 𝐴 ⟩ ∈ ◡ 𝐹 ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 ) )
5	4	adantl	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ⟨ ( 𝐹 ‘ 𝐴 ) , 𝐴 ⟩ ∈ ◡ 𝐹 ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 ) )
6	1 5	mpbird	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ⟨ ( 𝐹 ‘ 𝐴 ) , 𝐴 ⟩ ∈ ◡ 𝐹 )
7		elimasng	⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ V ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐴 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ↔ ⟨ ( 𝐹 ‘ 𝐴 ) , 𝐴 ⟩ ∈ ◡ 𝐹 ) )
8	2 7	mpan	⊢ ( 𝐴 ∈ dom 𝐹 → ( 𝐴 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ↔ ⟨ ( 𝐹 ‘ 𝐴 ) , 𝐴 ⟩ ∈ ◡ 𝐹 ) )
9	8	adantl	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐴 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ↔ ⟨ ( 𝐹 ‘ 𝐴 ) , 𝐴 ⟩ ∈ ◡ 𝐹 ) )
10	6 9	mpbird	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → 𝐴 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) )
11	2	snss	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝐵 )
12		imass2	⊢ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝐵 → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ⊆ ( ◡ 𝐹 “ 𝐵 ) )
13	11 12	sylbi	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ⊆ ( ◡ 𝐹 “ 𝐵 ) )
14	13	sseld	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → ( 𝐴 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) → 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )
15	10 14	syl5com	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )
16		fvimacnvi	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 )
17	16	ex	⊢ ( Fun 𝐹 → ( 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) )
18	17	adantr	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) )
19	15 18	impbid	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )