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

Metamath Proof Explorer

Theorem mndlactf1o

Description: An element X of a monoid E is invertible iff its left-translation F is bijective. See also grplactf1o . Remark in chapter I. of BourbakiAlg1 p. 17. (Contributed by Thierry Arnoux, 3-Aug-2025)

Ref Expression
Hypotheses mndlactf1o.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
mndlactf1o.z ⊢ 0 = ( 0g ‘ 𝐸 )
mndlactf1o.p ⊢ + = ( +g ‘ 𝐸 )
mndlactf1o.f ⊢ 𝐹 = ( 𝑎 ∈ 𝐵 ↦ ( 𝑋 + 𝑎 ) )
mndlactf1o.e ⊢ ( 𝜑 → 𝐸 ∈ Mnd )
mndlactf1o.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion mndlactf1o ( 𝜑 → ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 mndlactf1o.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
2 mndlactf1o.z ⊢ 0 = ( 0g ‘ 𝐸 )
3 mndlactf1o.p ⊢ + = ( +g ‘ 𝐸 )
4 mndlactf1o.f ⊢ 𝐹 = ( 𝑎 ∈ 𝐵 ↦ ( 𝑋 + 𝑎 ) )
5 mndlactf1o.e ⊢ ( 𝜑 → 𝐸 ∈ Mnd )
6 mndlactf1o.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 oveq2 ⊢ ( 𝑦 = 𝑢 → ( 𝑋 + 𝑦 ) = ( 𝑋 + 𝑢 ) )
8 7 eqeq1d ⊢ ( 𝑦 = 𝑢 → ( ( 𝑋 + 𝑦 ) = 0 ↔ ( 𝑋 + 𝑢 ) = 0 ) )
9 oveq1 ⊢ ( 𝑦 = 𝑢 → ( 𝑦 + 𝑋 ) = ( 𝑢 + 𝑋 ) )
10 9 eqeq1d ⊢ ( 𝑦 = 𝑢 → ( ( 𝑦 + 𝑋 ) = 0 ↔ ( 𝑢 + 𝑋 ) = 0 ) )
11 8 10 anbi12d ⊢ ( 𝑦 = 𝑢 → ( ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ↔ ( ( 𝑋 + 𝑢 ) = 0 ∧ ( 𝑢 + 𝑋 ) = 0 ) ) )
12 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → 𝑢 ∈ 𝐵 )
13 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → ( 𝑋 + 𝑢 ) = 0 )
14 5 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → 𝐸 ∈ Mnd )
15 6 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → 𝑋 ∈ 𝐵 )
16 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → 𝑣 ∈ 𝐵 )
17 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → ( 𝑣 + 𝑋 ) = 0 )
18 1 2 3 14 15 16 12 17 13 mndlrinv ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → 𝑣 = 𝑢 )
19 18 oveq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → ( 𝑣 + 𝑋 ) = ( 𝑢 + 𝑋 ) )
20 19 17 eqtr3d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → ( 𝑢 + 𝑋 ) = 0 )
21 13 20 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → ( ( 𝑋 + 𝑢 ) = 0 ∧ ( 𝑢 + 𝑋 ) = 0 ) )
22 11 12 21 rspcedvdw ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) )
23 f1ofo ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 → 𝐹 : 𝐵 –onto→ 𝐵 )
24 23 adantl ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → 𝐹 : 𝐵 –onto→ 𝐵 )
25 1 2 3 4 5 6 mndlactfo ⊢ ( 𝜑 → ( 𝐹 : 𝐵 –onto→ 𝐵 ↔ ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 ) )
26 25 biimpa ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –onto→ 𝐵 ) → ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 )
27 24 26 syldan ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 )
28 27 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) → ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 )
29 22 28 r19.29a ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) → ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) )
30 oveq1 ⊢ ( 𝑣 = ( ◡ 𝐹 ‘ 0 ) → ( 𝑣 + 𝑋 ) = ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) )
31 30 eqeq1d ⊢ ( 𝑣 = ( ◡ 𝐹 ‘ 0 ) → ( ( 𝑣 + 𝑋 ) = 0 ↔ ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) = 0 ) )
32 f1ocnv ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
33 f1of ⊢ ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 ⟶ 𝐵 )
34 32 33 syl ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 ⟶ 𝐵 )
35 34 adantl ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ◡ 𝐹 : 𝐵 ⟶ 𝐵 )
36 1 2 mndidcl ⊢ ( 𝐸 ∈ Mnd → 0 ∈ 𝐵 )
37 5 36 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → 0 ∈ 𝐵 )
39 35 38 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( ◡ 𝐹 ‘ 0 ) ∈ 𝐵 )
40 f1of1 ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 → 𝐹 : 𝐵 –1-1→ 𝐵 )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → 𝐹 : 𝐵 –1-1→ 𝐵 )
42 5 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → 𝐸 ∈ Mnd )
43 6 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → 𝑋 ∈ 𝐵 )
44 1 3 42 39 43 mndcld ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) ∈ 𝐵 )
45 44 38 jca ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) ∈ 𝐵 ∧ 0 ∈ 𝐵 ) )
46 1 3 2 mndrid ⊢ ( ( 𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + 0 ) = 𝑋 )
47 42 43 46 syl2anc ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝑋 + 0 ) = 𝑋 )
48 oveq2 ⊢ ( 𝑎 = 0 → ( 𝑋 + 𝑎 ) = ( 𝑋 + 0 ) )
49 ovexd ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝑋 + 0 ) ∈ V )
50 4 48 38 49 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝐹 ‘ 0 ) = ( 𝑋 + 0 ) )
51 oveq2 ⊢ ( 𝑎 = ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) → ( 𝑋 + 𝑎 ) = ( 𝑋 + ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) ) )
52 ovexd ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝑋 + ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) ) ∈ V )
53 4 51 44 52 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) ) = ( 𝑋 + ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) ) )
54 oveq2 ⊢ ( 𝑎 = ( ◡ 𝐹 ‘ 0 ) → ( 𝑋 + 𝑎 ) = ( 𝑋 + ( ◡ 𝐹 ‘ 0 ) ) )
55 ovexd ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝑋 + ( ◡ 𝐹 ‘ 0 ) ) ∈ V )
56 4 54 39 55 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 0 ) ) = ( 𝑋 + ( ◡ 𝐹 ‘ 0 ) ) )
57 simpr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
58 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ 0 ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 0 ) ) = 0 )
59 57 38 58 syl2anc ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 0 ) ) = 0 )
60 56 59 eqtr3d ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝑋 + ( ◡ 𝐹 ‘ 0 ) ) = 0 )
61 60 oveq1d ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( ( 𝑋 + ( ◡ 𝐹 ‘ 0 ) ) + 𝑋 ) = ( 0 + 𝑋 ) )
62 1 3 42 43 39 43 mndassd ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( ( 𝑋 + ( ◡ 𝐹 ‘ 0 ) ) + 𝑋 ) = ( 𝑋 + ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) ) )
63 1 3 2 mndlid ⊢ ( ( 𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ) → ( 0 + 𝑋 ) = 𝑋 )
64 42 43 63 syl2anc ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( 0 + 𝑋 ) = 𝑋 )
65 61 62 64 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝑋 + ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) ) = 𝑋 )
66 53 65 eqtrd ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) ) = 𝑋 )
67 47 50 66 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) ) = ( 𝐹 ‘ 0 ) )
68 f1fveq ⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐵 ∧ ( ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) ∈ 𝐵 ∧ 0 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) ) = ( 𝐹 ‘ 0 ) ↔ ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) = 0 ) )
69 68 biimpa ⊢ ( ( ( 𝐹 : 𝐵 –1-1→ 𝐵 ∧ ( ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) ∈ 𝐵 ∧ 0 ∈ 𝐵 ) ) ∧ ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) ) = ( 𝐹 ‘ 0 ) ) → ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) = 0 )
70 41 45 67 69 syl21anc ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ( ( ◡ 𝐹 ‘ 0 ) + 𝑋 ) = 0 )
71 31 39 70 rspcedvdw ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑋 ) = 0 )
72 29 71 r19.29a ⊢ ( ( 𝜑 ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) )
73 oveq1 ⊢ ( 𝑣 = 𝑦 → ( 𝑣 + 𝑋 ) = ( 𝑦 + 𝑋 ) )
74 73 eqeq1d ⊢ ( 𝑣 = 𝑦 → ( ( 𝑣 + 𝑋 ) = 0 ↔ ( 𝑦 + 𝑋 ) = 0 ) )
75 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ) → 𝑦 ∈ 𝐵 )
76 simprr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ) → ( 𝑦 + 𝑋 ) = 0 )
77 74 75 76 rspcedvdw ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ) → ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑋 ) = 0 )
78 oveq2 ⊢ ( 𝑢 = 𝑦 → ( 𝑋 + 𝑢 ) = ( 𝑋 + 𝑦 ) )
79 78 eqeq1d ⊢ ( 𝑢 = 𝑦 → ( ( 𝑋 + 𝑢 ) = 0 ↔ ( 𝑋 + 𝑦 ) = 0 ) )
80 simprl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ) → ( 𝑋 + 𝑦 ) = 0 )
81 79 75 80 rspcedvdw ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ) → ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 )
82 77 81 jca ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ) → ( ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑋 ) = 0 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 ) )
83 82 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ) → ( ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑋 ) = 0 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 ) )
84 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) → 𝐸 ∈ Mnd )
85 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) → 𝑋 ∈ 𝐵 )
86 simplr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) → 𝑣 ∈ 𝐵 )
87 simpr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) → ( 𝑣 + 𝑋 ) = 0 )
88 1 2 3 4 84 85 86 87 mndlactf1 ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) → 𝐹 : 𝐵 –1-1→ 𝐵 )
89 88 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑋 ) = 0 ) → 𝐹 : 𝐵 –1-1→ 𝐵 )
90 25 biimpar ⊢ ( ( 𝜑 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 ) → 𝐹 : 𝐵 –onto→ 𝐵 )
91 89 90 anim12dan ⊢ ( ( 𝜑 ∧ ( ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑋 ) = 0 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 ) ) → ( 𝐹 : 𝐵 –1-1→ 𝐵 ∧ 𝐹 : 𝐵 –onto→ 𝐵 ) )
92 df-f1o ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ↔ ( 𝐹 : 𝐵 –1-1→ 𝐵 ∧ 𝐹 : 𝐵 –onto→ 𝐵 ) )
93 91 92 sylibr ⊢ ( ( 𝜑 ∧ ( ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑋 ) = 0 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
94 83 93 syldan ⊢ ( ( 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
95 72 94 impbida ⊢ ( 𝜑 → ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ) )