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 ⊢ B ∈ ran ⁡ F → F '''' A = B → A F B

Proof

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