Metamath Proof Explorer

Theorem tz6.12i-afv2

Description: Corollary of Theorem 6.12(2) of TakeutiZaring p. 27. analogous to tz6.12i . (Contributed by AV, 5-Sep-2022)

Ref Expression
Assertion tz6.12i-afv2 ( 𝐵 ∈ ran 𝐹 → ( ( 𝐹 '''' 𝐴 ) = 𝐵 → 𝐴 𝐹 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( ( 𝐹 '''' 𝐴 ) = 𝑦 → ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ↔ 𝑦 ∈ ran 𝐹 ) )
2 dfatafv2rnb ⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 )
3 dfdfat2 ⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) )
4 3 simprbi ⊢ ( 𝐹 defAt 𝐴 → ∃! 𝑦 𝐴 𝐹 𝑦 )
5 2 4 sylbir ⊢ ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 → ∃! 𝑦 𝐴 𝐹 𝑦 )
6 tz6.12c-afv2 ⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( ( 𝐹 '''' 𝐴 ) = 𝑦 ↔ 𝐴 𝐹 𝑦 ) )
7 5 6 syl ⊢ ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 → ( ( 𝐹 '''' 𝐴 ) = 𝑦 ↔ 𝐴 𝐹 𝑦 ) )
8 7 biimpcd ⊢ ( ( 𝐹 '''' 𝐴 ) = 𝑦 → ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 → 𝐴 𝐹 𝑦 ) )
9 1 8 sylbird ⊢ ( ( 𝐹 '''' 𝐴 ) = 𝑦 → ( 𝑦 ∈ ran 𝐹 → 𝐴 𝐹 𝑦 ) )
10 9 eqcoms ⊢ ( 𝑦 = ( 𝐹 '''' 𝐴 ) → ( 𝑦 ∈ ran 𝐹 → 𝐴 𝐹 𝑦 ) )
11 eleq1 ⊢ ( 𝑦 = ( 𝐹 '''' 𝐴 ) → ( 𝑦 ∈ ran 𝐹 ↔ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ) )
12 breq2 ⊢ ( 𝑦 = ( 𝐹 '''' 𝐴 ) → ( 𝐴 𝐹 𝑦 ↔ 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) ) )
13 10 11 12 3imtr3d ⊢ ( 𝑦 = ( 𝐹 '''' 𝐴 ) → ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 → 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) ) )
14 13 vtocleg ⊢ ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 → ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 → 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) ) )
15 14 pm2.43i ⊢ ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 → 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) )
16 15 a1i ⊢ ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 → 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) ) )
17 eleq1 ⊢ ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ↔ 𝐵 ∈ ran 𝐹 ) )
18 breq2 ⊢ ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ( 𝐴 𝐹 ( 𝐹 '''' 𝐴 ) ↔ 𝐴 𝐹 𝐵 ) )
19 16 17 18 3imtr3d ⊢ ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ( 𝐵 ∈ ran 𝐹 → 𝐴 𝐹 𝐵 ) )
20 19 com12 ⊢ ( 𝐵 ∈ ran 𝐹 → ( ( 𝐹 '''' 𝐴 ) = 𝐵 → 𝐴 𝐹 𝐵 ) )