Metamath Proof Explorer


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 𝐹 ) → ( ( 𝐹𝐴 ) ∈ 𝐵𝐴 ∈ ( 𝐹𝐵 ) ) )