| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑦 = 𝑢 → (𝑋 + 𝑦) = (𝑋 + 𝑢)) | 
| 2 | 1 | eqeq1d 2739 | . . . . . 6
⊢ (𝑦 = 𝑢 → ((𝑋 + 𝑦) = 0 ↔ (𝑋 + 𝑢) = 0 )) | 
| 3 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑦 = 𝑢 → (𝑦 + 𝑋) = (𝑢 + 𝑋)) | 
| 4 | 3 | eqeq1d 2739 | . . . . . 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 33029 | . . . . . . . 8
⊢
((((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢 ∈ 𝐵) ∧ (𝑋 + 𝑢) = 0 ) → 𝑣 = 𝑢) | 
| 18 | 17 | oveq1d 7446 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢 ∈ 𝐵) ∧ (𝑋 + 𝑢) = 0 ) → (𝑣 + 𝑋) = (𝑢 + 𝑋)) | 
| 19 | 18, 16 | eqtr3d 2779 | . . . . . 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 6855 | . . . . . . 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 33032 | . . . . . . 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 3162 | . . 3
⊢ ((((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) → ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) | 
| 30 |  | oveq1 7438 | . . . . 5
⊢ (𝑣 = (◡𝐹‘ 0 ) → (𝑣 + 𝑋) = ((◡𝐹‘ 0 ) + 𝑋)) | 
| 31 | 30 | eqeq1d 2739 | . . . 4
⊢ (𝑣 = (◡𝐹‘ 0 ) → ((𝑣 + 𝑋) = 0 ↔ ((◡𝐹‘ 0 ) + 𝑋) = 0 )) | 
| 32 |  | f1ocnv 6860 | . . . . . . 7
⊢ (𝐹:𝐵–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐵) | 
| 33 |  | f1of 6848 | . . . . . . 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 18762 | . . . . . . 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 6847 | . . . . . 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 33027 | . . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → ((◡𝐹‘ 0 ) + 𝑋) ∈ 𝐵) | 
| 45 | 44, 38 | jca 511 | . . . . 5
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (((◡𝐹‘ 0 ) + 𝑋) ∈ 𝐵 ∧ 0 ∈ 𝐵)) | 
| 46 | 8, 10, 9 | mndrid 18768 | . . . . . . 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 2779 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (𝑋 + (◡𝐹‘ 0 )) = 0 ) | 
| 61 | 60 | oveq1d 7446 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐹‘ 0 )) + 𝑋) = ( 0 + 𝑋)) | 
| 62 | 8, 10, 42, 43, 39, 43 | mndassd 33028 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐹‘ 0 )) + 𝑋) = (𝑋 + ((◡𝐹‘ 0 ) + 𝑋))) | 
| 63 | 8, 10, 9 | mndlid 18767 | . . . . . . . . 9
⊢ ((𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) | 
| 64 | 42, 43, 63 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → ( 0 + 𝑋) = 𝑋) | 
| 65 | 61, 62, 64 | 3eqtr3d 2785 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (𝑋 + ((◡𝐹‘ 0 ) + 𝑋)) = 𝑋) | 
| 66 | 53, 65 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → (𝐹‘((◡𝐹‘ 0 ) + 𝑋)) = 𝑋) | 
| 67 | 47, 50, 66 | 3eqtr4rd 2788 | . . . . 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 3162 | . 2
⊢ ((𝜑 ∧ 𝐹:𝐵–1-1-onto→𝐵) → ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) | 
| 73 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑣 = 𝑦 → (𝑣 + 𝑋) = (𝑦 + 𝑋)) | 
| 74 | 73 | eqeq1d 2739 | . . . . . 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 2739 | . . . . . 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 3158 | . . 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 33031 | . . . . . 6
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑣 + 𝑋) = 0 ) → 𝐹:𝐵–1-1→𝐵) | 
| 89 | 88 | r19.29an 3158 | . . . . 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 6568 | . . . 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 ))) |