This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tz6.12i

Description: Corollary of Theorem 6.12(2) of TakeutiZaring p. 27. (Contributed by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion tz6.12i ( 𝐵 ≠ ∅ → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 → 𝐴 𝐹 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
2 neeq1 ⊢ ( ( 𝐹 ‘ 𝐴 ) = 𝑦 → ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ ↔ 𝑦 ≠ ∅ ) )
3 tz6.12-2 ⊢ ( ¬ ∃! 𝑦 𝐴 𝐹 𝑦 → ( 𝐹 ‘ 𝐴 ) = ∅ )
4 3 necon1ai ⊢ ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ → ∃! 𝑦 𝐴 𝐹 𝑦 )
5 tz6.12c ⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( ( 𝐹 ‘ 𝐴 ) = 𝑦 ↔ 𝐴 𝐹 𝑦 ) )
6 4 5 syl ⊢ ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ → ( ( 𝐹 ‘ 𝐴 ) = 𝑦 ↔ 𝐴 𝐹 𝑦 ) )
7 6 biimpcd ⊢ ( ( 𝐹 ‘ 𝐴 ) = 𝑦 → ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ → 𝐴 𝐹 𝑦 ) )
8 2 7 sylbird ⊢ ( ( 𝐹 ‘ 𝐴 ) = 𝑦 → ( 𝑦 ≠ ∅ → 𝐴 𝐹 𝑦 ) )
9 8 eqcoms ⊢ ( 𝑦 = ( 𝐹 ‘ 𝐴 ) → ( 𝑦 ≠ ∅ → 𝐴 𝐹 𝑦 ) )
10 neeq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝐴 ) → ( 𝑦 ≠ ∅ ↔ ( 𝐹 ‘ 𝐴 ) ≠ ∅ ) )
11 breq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝐴 ) → ( 𝐴 𝐹 𝑦 ↔ 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ) )
12 9 10 11 3imtr3d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝐴 ) → ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ → 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ) )
13 1 12 vtocle ⊢ ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ → 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) )
14 13 a1i ⊢ ( ( 𝐹 ‘ 𝐴 ) = 𝐵 → ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ → 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ) )
15 neeq1 ⊢ ( ( 𝐹 ‘ 𝐴 ) = 𝐵 → ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ ↔ 𝐵 ≠ ∅ ) )
16 breq2 ⊢ ( ( 𝐹 ‘ 𝐴 ) = 𝐵 → ( 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ↔ 𝐴 𝐹 𝐵 ) )
17 14 15 16 3imtr3d ⊢ ( ( 𝐹 ‘ 𝐴 ) = 𝐵 → ( 𝐵 ≠ ∅ → 𝐴 𝐹 𝐵 ) )
18 17 com12 ⊢ ( 𝐵 ≠ ∅ → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 → 𝐴 𝐹 𝐵 ) )