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 ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A ∈ B ↔ A ∈ F -1 B

Proof

Step Hyp Ref Expression
1 snssi ⊢ A ∈ dom ⁡ F → A ⊆ dom ⁡ F
2 funimass3 ⊢ Fun ⁡ F ∧ A ⊆ dom ⁡ F → F A ⊆ B ↔ A ⊆ F -1 B
3 1 2 sylan2 ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F A ⊆ B ↔ A ⊆ F -1 B
4 fvex ⊢ F ⁡ A ∈ V
5 4 snss ⊢ F ⁡ A ∈ B ↔ F ⁡ A ⊆ B
6 eqid ⊢ dom ⁡ F = dom ⁡ F
7 df-fn ⊢ F Fn dom ⁡ F ↔ Fun ⁡ F ∧ dom ⁡ F = dom ⁡ F
8 7 biimpri ⊢ Fun ⁡ F ∧ dom ⁡ F = dom ⁡ F → F Fn dom ⁡ F
9 6 8 mpan2 ⊢ Fun ⁡ F → F Fn dom ⁡ F
10 fnsnfv ⊢ F Fn dom ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A = F A
11 9 10 sylan ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A = F A
12 11 sseq1d ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A ⊆ B ↔ F A ⊆ B
13 5 12 bitrid ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A ∈ B ↔ F A ⊆ B
14 snssg ⊢ A ∈ dom ⁡ F → A ∈ F -1 B ↔ A ⊆ F -1 B
15 14 adantl ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → A ∈ F -1 B ↔ A ⊆ F -1 B
16 3 13 15 3bitr4d ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A ∈ B ↔ A ∈ F -1 B