Step | Hyp | Ref
| Expression |
1 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑦 = 𝑢 → (𝑋 + 𝑦) = (𝑋 + 𝑢)) |
2 | 1 | eqeq1d 2737 |
. . . . . 6
⊢ (𝑦 = 𝑢 → ((𝑋 + 𝑦) = 0 ↔ (𝑋 + 𝑢) = 0 )) |
3 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑦 = 𝑢 → (𝑦 + 𝑋) = (𝑢 + 𝑋)) |
4 | 3 | eqeq1d 2737 |
. . . . . 6
⊢ (𝑦 = 𝑢 → ((𝑦 + 𝑋) = 0 ↔ (𝑢 + 𝑋) = 0 )) |
5 | 2, 4 | anbi12d 632 |
. . . . 5
⊢ (𝑦 = 𝑢 → (((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 ) ↔ ((𝑋 + 𝑢) = 0 ∧ (𝑢 + 𝑋) = 0 ))) |
6 | | simplr 769 |
. . . . 5
⊢
((((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢 ∈ 𝐵) ∧ (𝑋 + 𝑢) = 0 ) → 𝑢 ∈ 𝐵) |
7 | | simpr 484 |
. . . . . 6
⊢
((((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢 ∈ 𝐵) ∧ (𝑋 + 𝑢) = 0 ) → (𝑋 + 𝑢) = 0 ) |
8 | | mndlactf1o.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐸) |
9 | | mndlactf1o.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐸) |
10 | | mndlactf1o.p |
. . . . . . . . 9
⊢ + =
(+g‘𝐸) |
11 | | mndlactf1o.e |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ Mnd) |
12 | 11 | ad5antr 734 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢 ∈ 𝐵) ∧ (𝑋 + 𝑢) = 0 ) → 𝐸 ∈ Mnd) |
13 | | mndlactf1o.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
14 | 13 | ad5antr 734 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢 ∈ 𝐵) ∧ (𝑋 + 𝑢) = 0 ) → 𝑋 ∈ 𝐵) |
15 | | simp-4r 784 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢 ∈ 𝐵) ∧ (𝑋 + 𝑢) = 0 ) → 𝑣 ∈ 𝐵) |
16 | | simpllr 776 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢 ∈ 𝐵) ∧ (𝑋 + 𝑢) = 0 ) → (𝑣 + 𝑋) = 0 ) |
17 | 8, 9, 10, 12, 14, 15, 6, 16, 7 | mndlrinv 33012 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢 ∈ 𝐵) ∧ (𝑋 + 𝑢) = 0 ) → 𝑣 = 𝑢) |
18 | 17 | oveq1d 7446 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢 ∈ 𝐵) ∧ (𝑋 + 𝑢) = 0 ) → (𝑣 + 𝑋) = (𝑢 + 𝑋)) |
19 | 18, 16 | eqtr3d 2777 |
. . . . . 6
⊢
((((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢 ∈ 𝐵) ∧ (𝑋 + 𝑢) = 0 ) → (𝑢 + 𝑋) = 0 ) |
20 | 7, 19 | jca 511 |
. . . . 5
⊢
((((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢 ∈ 𝐵) ∧ (𝑋 + 𝑢) = 0 ) → ((𝑋 + 𝑢) = 0 ∧ (𝑢 + 𝑋) = 0 )) |
21 | 5, 6, 20 | rspcedvdw 3625 |
. . . 4
⊢
((((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢 ∈ 𝐵) ∧ (𝑋 + 𝑢) = 0 ) → ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) |
22 | | f1ofo 6856 |
. . . . . . 7
⊢ (𝐹:𝐵–1-1-onto→𝐵 → 𝐹:𝐵–onto→𝐵) |
23 | 22 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → 𝐹:𝐵–onto→𝐵) |
24 | | mndlactf1o.f |
. . . . . . . 8
⊢ 𝐹 = (𝑎 ∈ 𝐵 ↦ (𝑋 + 𝑎)) |
25 | 8, 9, 10, 24, 11, 13 | mndlactfo 33015 |
. . . . . . 7
⊢ (𝜑 → (𝐹:𝐵–onto→𝐵 ↔ ∃𝑢 ∈ 𝐵 (𝑋 + 𝑢) = 0 )) |
26 | 25 | biimpa 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝐵–onto→𝐵) → ∃𝑢 ∈ 𝐵 (𝑋 + 𝑢) = 0 ) |
27 | 23, 26 | syldan 591 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → ∃𝑢 ∈ 𝐵 (𝑋 + 𝑢) = 0 ) |
28 | 27 | ad2antrr 726 |
. . . 4
⊢ ((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) → ∃𝑢 ∈ 𝐵 (𝑋 + 𝑢) = 0 ) |
29 | 21, 28 | r19.29a 3160 |
. . 3
⊢ ((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) → ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) |
30 | | oveq1 7438 |
. . . . 5
⊢ (𝑣 = (◡𝐹‘ 0 ) → (𝑣 + 𝑋) = ((◡𝐹‘ 0 ) + 𝑋)) |
31 | 30 | eqeq1d 2737 |
. . . 4
⊢ (𝑣 = (◡𝐹‘ 0 ) → ((𝑣 + 𝑋) = 0 ↔ ((◡𝐹‘ 0 ) + 𝑋) = 0 )) |
32 | | f1ocnv 6861 |
. . . . . . 7
⊢ (𝐹:𝐵–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐵) |
33 | | f1of 6849 |
. . . . . . 7
⊢ (◡𝐹:𝐵–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐵) |
34 | 32, 33 | syl 17 |
. . . . . 6
⊢ (𝐹:𝐵–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐵) |
35 | 34 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → ◡𝐹:𝐵⟶𝐵) |
36 | 8, 9 | mndidcl 18775 |
. . . . . . 7
⊢ (𝐸 ∈ Mnd → 0 ∈ 𝐵) |
37 | 11, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 ∈ 𝐵) |
38 | 37 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → 0 ∈ 𝐵) |
39 | 35, 38 | ffvelcdmd 7105 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (◡𝐹‘ 0 ) ∈ 𝐵) |
40 | | f1of1 6848 |
. . . . . 6
⊢ (𝐹:𝐵–1-1-onto→𝐵 → 𝐹:𝐵–1-1→𝐵) |
41 | 40 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → 𝐹:𝐵–1-1→𝐵) |
42 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → 𝐸 ∈ Mnd) |
43 | 13 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → 𝑋 ∈ 𝐵) |
44 | 8, 10, 42, 39, 43 | mndcld 33010 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → ((◡𝐹‘ 0 ) + 𝑋) ∈ 𝐵) |
45 | 44, 38 | jca 511 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (((◡𝐹‘ 0 ) + 𝑋) ∈ 𝐵 ∧ 0 ∈ 𝐵)) |
46 | 8, 10, 9 | mndrid 18781 |
. . . . . . 7
⊢ ((𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋) |
47 | 42, 43, 46 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (𝑋 + 0 ) = 𝑋) |
48 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑎 = 0 → (𝑋 + 𝑎) = (𝑋 + 0 )) |
49 | | ovexd 7466 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (𝑋 + 0 ) ∈
V) |
50 | 24, 48, 38, 49 | fvmptd3 7039 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (𝐹‘ 0 ) = (𝑋 + 0 )) |
51 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑎 = ((◡𝐹‘ 0 ) + 𝑋) → (𝑋 + 𝑎) = (𝑋 + ((◡𝐹‘ 0 ) + 𝑋))) |
52 | | ovexd 7466 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (𝑋 + ((◡𝐹‘ 0 ) + 𝑋)) ∈ V) |
53 | 24, 51, 44, 52 | fvmptd3 7039 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (𝐹‘((◡𝐹‘ 0 ) + 𝑋)) = (𝑋 + ((◡𝐹‘ 0 ) + 𝑋))) |
54 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑎 = (◡𝐹‘ 0 ) → (𝑋 + 𝑎) = (𝑋 + (◡𝐹‘ 0 ))) |
55 | | ovexd 7466 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (𝑋 + (◡𝐹‘ 0 )) ∈
V) |
56 | 24, 54, 39, 55 | fvmptd3 7039 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (𝐹‘(◡𝐹‘ 0 )) = (𝑋 + (◡𝐹‘ 0 ))) |
57 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → 𝐹:𝐵–1-1-onto→𝐵) |
58 | | f1ocnvfv2 7297 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ 0 ∈ 𝐵) → (𝐹‘(◡𝐹‘ 0 )) = 0 ) |
59 | 57, 38, 58 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (𝐹‘(◡𝐹‘ 0 )) = 0 ) |
60 | 56, 59 | eqtr3d 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (𝑋 + (◡𝐹‘ 0 )) = 0 ) |
61 | 60 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐹‘ 0 )) + 𝑋) = ( 0 + 𝑋)) |
62 | 8, 10, 42, 43, 39, 43 | mndassd 33011 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐹‘ 0 )) + 𝑋) = (𝑋 + ((◡𝐹‘ 0 ) + 𝑋))) |
63 | 8, 10, 9 | mndlid 18780 |
. . . . . . . . 9
⊢ ((𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) |
64 | 42, 43, 63 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → ( 0 + 𝑋) = 𝑋) |
65 | 61, 62, 64 | 3eqtr3d 2783 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (𝑋 + ((◡𝐹‘ 0 ) + 𝑋)) = 𝑋) |
66 | 53, 65 | eqtrd 2775 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (𝐹‘((◡𝐹‘ 0 ) + 𝑋)) = 𝑋) |
67 | 47, 50, 66 | 3eqtr4rd 2786 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (𝐹‘((◡𝐹‘ 0 ) + 𝑋)) = (𝐹‘ 0 )) |
68 | | f1fveq 7282 |
. . . . . 6
⊢ ((𝐹:𝐵–1-1→𝐵 ∧ (((◡𝐹‘ 0 ) + 𝑋) ∈ 𝐵 ∧ 0 ∈ 𝐵)) → ((𝐹‘((◡𝐹‘ 0 ) + 𝑋)) = (𝐹‘ 0 ) ↔ ((◡𝐹‘ 0 ) + 𝑋) = 0 )) |
69 | 68 | biimpa 476 |
. . . . 5
⊢ (((𝐹:𝐵–1-1→𝐵 ∧ (((◡𝐹‘ 0 ) + 𝑋) ∈ 𝐵 ∧ 0 ∈ 𝐵)) ∧ (𝐹‘((◡𝐹‘ 0 ) + 𝑋)) = (𝐹‘ 0 )) → ((◡𝐹‘ 0 ) + 𝑋) = 0 ) |
70 | 41, 45, 67, 69 | syl21anc 838 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → ((◡𝐹‘ 0 ) + 𝑋) = 0 ) |
71 | 31, 39, 70 | rspcedvdw 3625 |
. . 3
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → ∃𝑣 ∈ 𝐵 (𝑣 + 𝑋) = 0 ) |
72 | 29, 71 | r19.29a 3160 |
. 2
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) |
73 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑣 = 𝑦 → (𝑣 + 𝑋) = (𝑦 + 𝑋)) |
74 | 73 | eqeq1d 2737 |
. . . . . 6
⊢ (𝑣 = 𝑦 → ((𝑣 + 𝑋) = 0 ↔ (𝑦 + 𝑋) = 0 )) |
75 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → 𝑦 ∈ 𝐵) |
76 | | simprr 773 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → (𝑦 + 𝑋) = 0 ) |
77 | 74, 75, 76 | rspcedvdw 3625 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → ∃𝑣 ∈ 𝐵 (𝑣 + 𝑋) = 0 ) |
78 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑢 = 𝑦 → (𝑋 + 𝑢) = (𝑋 + 𝑦)) |
79 | 78 | eqeq1d 2737 |
. . . . . 6
⊢ (𝑢 = 𝑦 → ((𝑋 + 𝑢) = 0 ↔ (𝑋 + 𝑦) = 0 )) |
80 | | simprl 771 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → (𝑋 + 𝑦) = 0 ) |
81 | 79, 75, 80 | rspcedvdw 3625 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → ∃𝑢 ∈ 𝐵 (𝑋 + 𝑢) = 0 ) |
82 | 77, 81 | jca 511 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → (∃𝑣 ∈ 𝐵 (𝑣 + 𝑋) = 0 ∧ ∃𝑢 ∈ 𝐵 (𝑋 + 𝑢) = 0 )) |
83 | 82 | r19.29an 3156 |
. . 3
⊢ ((𝜑 ∧ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → (∃𝑣 ∈ 𝐵 (𝑣 + 𝑋) = 0 ∧ ∃𝑢 ∈ 𝐵 (𝑋 + 𝑢) = 0 )) |
84 | 11 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) → 𝐸 ∈ Mnd) |
85 | 13 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) → 𝑋 ∈ 𝐵) |
86 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) → 𝑣 ∈ 𝐵) |
87 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) → (𝑣 + 𝑋) = 0 ) |
88 | 8, 9, 10, 24, 84, 85, 86, 87 | mndlactf1 33014 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) → 𝐹:𝐵–1-1→𝐵) |
89 | 88 | r19.29an 3156 |
. . . . 5
⊢ ((𝜑 ∧ ∃𝑣 ∈ 𝐵 (𝑣 + 𝑋) = 0 ) → 𝐹:𝐵–1-1→𝐵) |
90 | 25 | biimpar 477 |
. . . . 5
⊢ ((𝜑 ∧ ∃𝑢 ∈ 𝐵 (𝑋 + 𝑢) = 0 ) → 𝐹:𝐵–onto→𝐵) |
91 | 89, 90 | anim12dan 619 |
. . . 4
⊢ ((𝜑 ∧ (∃𝑣 ∈ 𝐵 (𝑣 + 𝑋) = 0 ∧ ∃𝑢 ∈ 𝐵 (𝑋 + 𝑢) = 0 )) → (𝐹:𝐵–1-1→𝐵 ∧ 𝐹:𝐵–onto→𝐵)) |
92 | | df-f1o 6570 |
. . . 4
⊢ (𝐹:𝐵–1-1-onto→𝐵 ↔ (𝐹:𝐵–1-1→𝐵 ∧ 𝐹:𝐵–onto→𝐵)) |
93 | 91, 92 | sylibr 234 |
. . 3
⊢ ((𝜑 ∧ (∃𝑣 ∈ 𝐵 (𝑣 + 𝑋) = 0 ∧ ∃𝑢 ∈ 𝐵 (𝑋 + 𝑢) = 0 )) → 𝐹:𝐵–1-1-onto→𝐵) |
94 | 83, 93 | syldan 591 |
. 2
⊢ ((𝜑 ∧ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → 𝐹:𝐵–1-1-onto→𝐵) |
95 | 72, 94 | impbida 801 |
1
⊢ (𝜑 → (𝐹:𝐵–1-1-onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 ))) |