This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvimacnvALT

Description: Alternate proof of fvimacnv , based on funimass3 . If funimass3 is ever proved directly, as opposed to using funimacnv pointwise, then the proof of funimacnv should be replaced with this one. (Contributed by Raph Levien, 20-Nov-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion fvimacnvALT ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 snssi ⊢ ( 𝐴 ∈ dom 𝐹 → { 𝐴 } ⊆ dom 𝐹 )
2 funimass3 ⊢ ( ( Fun 𝐹 ∧ { 𝐴 } ⊆ dom 𝐹 ) → ( ( 𝐹 “ { 𝐴 } ) ⊆ 𝐵 ↔ { 𝐴 } ⊆ ( ◡ 𝐹 “ 𝐵 ) ) )
3 1 2 sylan2 ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 “ { 𝐴 } ) ⊆ 𝐵 ↔ { 𝐴 } ⊆ ( ◡ 𝐹 “ 𝐵 ) ) )
4 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
5 4 snss ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝐵 )
6 eqid ⊢ dom 𝐹 = dom 𝐹
7 df-fn ⊢ ( 𝐹 Fn dom 𝐹 ↔ ( Fun 𝐹 ∧ dom 𝐹 = dom 𝐹 ) )
8 7 biimpri ⊢ ( ( Fun 𝐹 ∧ dom 𝐹 = dom 𝐹 ) → 𝐹 Fn dom 𝐹 )
9 6 8 mpan2 ⊢ ( Fun 𝐹 → 𝐹 Fn dom 𝐹 )
10 fnsnfv ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → { ( 𝐹 ‘ 𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )
11 9 10 sylan ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → { ( 𝐹 ‘ 𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )
12 11 sseq1d ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝐵 ↔ ( 𝐹 “ { 𝐴 } ) ⊆ 𝐵 ) )
13 5 12 bitrid ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ ( 𝐹 “ { 𝐴 } ) ⊆ 𝐵 ) )
14 snssg ⊢ ( 𝐴 ∈ dom 𝐹 → ( 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ↔ { 𝐴 } ⊆ ( ◡ 𝐹 “ 𝐵 ) ) )
15 14 adantl ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ↔ { 𝐴 } ⊆ ( ◡ 𝐹 “ 𝐵 ) ) )
16 3 13 15 3bitr4d ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )