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