Metamath Proof Explorer

Theorem dfatbrafv2b

Description: Equivalence of function value and binary relation, analogous to fnbrfvb or funbrfvb . B e. _V is required, because otherwise A F B <-> (/) e. F can be true, but ( F '''' A ) = B is always false (because of dfatafv2ex ). (Contributed by AV, 6-Sep-2022)

Ref Expression
Assertion dfatbrafv2b ( ( 𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐹 '''' 𝐴 ) = 𝐵 ↔ 𝐴 𝐹 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 𝐹 '''' 𝐴 ) = ( 𝐹 '''' 𝐴 )
2 dfatafv2ex ⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) ∈ V )
3 2 adantr ⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐹 '''' 𝐴 ) ∈ V )
4 eqeq2 ⊢ ( 𝑥 = ( 𝐹 '''' 𝐴 ) → ( ( 𝐹 '''' 𝐴 ) = 𝑥 ↔ ( 𝐹 '''' 𝐴 ) = ( 𝐹 '''' 𝐴 ) ) )
5 breq2 ⊢ ( 𝑥 = ( 𝐹 '''' 𝐴 ) → ( 𝐴 𝐹 𝑥 ↔ 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) ) )
6 4 5 bibi12d ⊢ ( 𝑥 = ( 𝐹 '''' 𝐴 ) → ( ( ( 𝐹 '''' 𝐴 ) = 𝑥 ↔ 𝐴 𝐹 𝑥 ) ↔ ( ( 𝐹 '''' 𝐴 ) = ( 𝐹 '''' 𝐴 ) ↔ 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) ) ) )
7 6 adantl ⊢ ( ( ( 𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑥 = ( 𝐹 '''' 𝐴 ) ) → ( ( ( 𝐹 '''' 𝐴 ) = 𝑥 ↔ 𝐴 𝐹 𝑥 ) ↔ ( ( 𝐹 '''' 𝐴 ) = ( 𝐹 '''' 𝐴 ) ↔ 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) ) ) )
8 dfdfat2 ⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) )
9 tz6.12c-afv2 ⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( ( 𝐹 '''' 𝐴 ) = 𝑥 ↔ 𝐴 𝐹 𝑥 ) )
10 8 9 simplbiim ⊢ ( 𝐹 defAt 𝐴 → ( ( 𝐹 '''' 𝐴 ) = 𝑥 ↔ 𝐴 𝐹 𝑥 ) )
11 10 adantr ⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐹 '''' 𝐴 ) = 𝑥 ↔ 𝐴 𝐹 𝑥 ) )
12 3 7 11 vtocld ⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐹 '''' 𝐴 ) = ( 𝐹 '''' 𝐴 ) ↔ 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) ) )
13 1 12 mpbii ⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) )
14 breq2 ⊢ ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ( 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) ↔ 𝐴 𝐹 𝐵 ) )
15 13 14 syl5ibcom ⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐹 '''' 𝐴 ) = 𝐵 → 𝐴 𝐹 𝐵 ) )
16 df-dfat ⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
17 simpll ⊢ ( ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ∈ dom 𝐹 )
18 simpr ⊢ ( ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐵 ∈ 𝑊 ) → 𝐵 ∈ 𝑊 )
19 simpr ⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → Fun ( 𝐹 ↾ { 𝐴 } ) )
20 19 adantr ⊢ ( ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐵 ∈ 𝑊 ) → Fun ( 𝐹 ↾ { 𝐴 } ) )
21 17 18 20 jca31 ⊢ ( ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
22 16 21 sylanb ⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
23 funressnbrafv2 ⊢ ( ( ( 𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐴 𝐹 𝐵 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) )
24 22 23 syl ⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 𝐹 𝐵 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) )
25 15 24 impbid ⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐹 '''' 𝐴 ) = 𝐵 ↔ 𝐴 𝐹 𝐵 ) )