Theorem bj-fvimacnv0

Description: Variant of fvimacnv where membership of A in the domain is not needed provided the containing class B does not contain the empty set. Note that this antecedent would not be needed with Definition df-afv . (Contributed by BJ, 7-Jan-2024)

	Ref	Expression
Assertion	bj-fvimacnv0	⊢ ( ( Fun 𝐹 ∧ ¬ ∅ ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( ( 𝐹 ‘ 𝐴 ) = ∅ → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ ∅ ∈ 𝐵 ) )
2	1	biimpcd	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → ( ( 𝐹 ‘ 𝐴 ) = ∅ → ∅ ∈ 𝐵 ) )
3	2	con3rr3	⊢ ( ¬ ∅ ∈ 𝐵 → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → ¬ ( 𝐹 ‘ 𝐴 ) = ∅ ) )
4	3	imp	⊢ ( ( ¬ ∅ ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) → ¬ ( 𝐹 ‘ 𝐴 ) = ∅ )
5		ndmfv	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )
6	4 5	nsyl2	⊢ ( ( ¬ ∅ ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) → 𝐴 ∈ dom 𝐹 )
7		simpr	⊢ ( ( ¬ ∅ ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 )
8		fvimacnv	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )
9	8	biimpd	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )
10	9	ex	⊢ ( Fun 𝐹 → ( 𝐴 ∈ dom 𝐹 → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) ) )
11	10	com3l	⊢ ( 𝐴 ∈ dom 𝐹 → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → ( Fun 𝐹 → 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) ) )
12	6 7 11	sylc	⊢ ( ( ¬ ∅ ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) → ( Fun 𝐹 → 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )
13	12	ex	⊢ ( ¬ ∅ ∈ 𝐵 → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → ( Fun 𝐹 → 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) ) )
14	13	com3r	⊢ ( Fun 𝐹 → ( ¬ ∅ ∈ 𝐵 → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) ) )
15	14	imp	⊢ ( ( Fun 𝐹 ∧ ¬ ∅ ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )
16		fvimacnvi	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 )
17	16	ex	⊢ ( Fun 𝐹 → ( 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) )
18	17	adantr	⊢ ( ( Fun 𝐹 ∧ ¬ ∅ ∈ 𝐵 ) → ( 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) )
19	15 18	impbid	⊢ ( ( Fun 𝐹 ∧ ¬ ∅ ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )