| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | vex 3483 | . . . . 5
⊢ 𝑥 ∈ V | 
| 2 |  | f1eq1 6798 | . . . . 5
⊢ (ℎ = 𝑥 → (ℎ:𝐴–1-1→𝐴 ↔ 𝑥:𝐴–1-1→𝐴)) | 
| 3 | 1, 2 | elab 3678 | . . . 4
⊢ (𝑥 ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴} ↔ 𝑥:𝐴–1-1→𝐴) | 
| 4 |  | f1f 6803 | . . . . 5
⊢ (𝑥:𝐴–1-1→𝐴 → 𝑥:𝐴⟶𝐴) | 
| 5 |  | sursubmefmnd.m | . . . . . 6
⊢ 𝑀 = (EndoFMnd‘𝐴) | 
| 6 |  | eqid 2736 | . . . . . 6
⊢
(Base‘𝑀) =
(Base‘𝑀) | 
| 7 | 5, 6 | elefmndbas 18887 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝑀) ↔ 𝑥:𝐴⟶𝐴)) | 
| 8 | 4, 7 | imbitrrid 246 | . . . 4
⊢ (𝐴 ∈ 𝑉 → (𝑥:𝐴–1-1→𝐴 → 𝑥 ∈ (Base‘𝑀))) | 
| 9 | 3, 8 | biimtrid 242 | . . 3
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴} → 𝑥 ∈ (Base‘𝑀))) | 
| 10 | 9 | ssrdv 3988 | . 2
⊢ (𝐴 ∈ 𝑉 → {ℎ ∣ ℎ:𝐴–1-1→𝐴} ⊆ (Base‘𝑀)) | 
| 11 | 5 | efmndid 18902 | . . 3
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) = (0g‘𝑀)) | 
| 12 |  | resiexg 7935 | . . . 4
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) | 
| 13 |  | f1oi 6885 | . . . . 5
⊢ ( I
↾ 𝐴):𝐴–1-1-onto→𝐴 | 
| 14 |  | f1of1 6846 | . . . . 5
⊢ (( I
↾ 𝐴):𝐴–1-1-onto→𝐴 → ( I ↾ 𝐴):𝐴–1-1→𝐴) | 
| 15 | 13, 14 | mp1i 13 | . . . 4
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴):𝐴–1-1→𝐴) | 
| 16 |  | f1eq1 6798 | . . . 4
⊢ (ℎ = ( I ↾ 𝐴) → (ℎ:𝐴–1-1→𝐴 ↔ ( I ↾ 𝐴):𝐴–1-1→𝐴)) | 
| 17 | 12, 15, 16 | elabd 3680 | . . 3
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴}) | 
| 18 | 11, 17 | eqeltrrd 2841 | . 2
⊢ (𝐴 ∈ 𝑉 → (0g‘𝑀) ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴}) | 
| 19 |  | vex 3483 | . . . . . 6
⊢ 𝑦 ∈ V | 
| 20 |  | f1eq1 6798 | . . . . . 6
⊢ (ℎ = 𝑦 → (ℎ:𝐴–1-1→𝐴 ↔ 𝑦:𝐴–1-1→𝐴)) | 
| 21 | 19, 20 | elab 3678 | . . . . 5
⊢ (𝑦 ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴} ↔ 𝑦:𝐴–1-1→𝐴) | 
| 22 | 3, 21 | anbi12i 628 | . . . 4
⊢ ((𝑥 ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴} ∧ 𝑦 ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴}) ↔ (𝑥:𝐴–1-1→𝐴 ∧ 𝑦:𝐴–1-1→𝐴)) | 
| 23 |  | f1co 6814 | . . . . . . 7
⊢ ((𝑥:𝐴–1-1→𝐴 ∧ 𝑦:𝐴–1-1→𝐴) → (𝑥 ∘ 𝑦):𝐴–1-1→𝐴) | 
| 24 | 23 | adantl 481 | . . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥:𝐴–1-1→𝐴 ∧ 𝑦:𝐴–1-1→𝐴)) → (𝑥 ∘ 𝑦):𝐴–1-1→𝐴) | 
| 25 |  | f1f 6803 | . . . . . . . . . . . 12
⊢ (𝑦:𝐴–1-1→𝐴 → 𝑦:𝐴⟶𝐴) | 
| 26 | 4, 25 | anim12i 613 | . . . . . . . . . . 11
⊢ ((𝑥:𝐴–1-1→𝐴 ∧ 𝑦:𝐴–1-1→𝐴) → (𝑥:𝐴⟶𝐴 ∧ 𝑦:𝐴⟶𝐴)) | 
| 27 | 5, 6 | elefmndbas 18887 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → (𝑦 ∈ (Base‘𝑀) ↔ 𝑦:𝐴⟶𝐴)) | 
| 28 | 7, 27 | anbi12d 632 | . . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀)) ↔ (𝑥:𝐴⟶𝐴 ∧ 𝑦:𝐴⟶𝐴))) | 
| 29 | 26, 28 | imbitrrid 246 | . . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ((𝑥:𝐴–1-1→𝐴 ∧ 𝑦:𝐴–1-1→𝐴) → (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀)))) | 
| 30 | 29 | imp 406 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥:𝐴–1-1→𝐴 ∧ 𝑦:𝐴–1-1→𝐴)) → (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀))) | 
| 31 |  | eqid 2736 | . . . . . . . . . 10
⊢
(+g‘𝑀) = (+g‘𝑀) | 
| 32 | 5, 6, 31 | efmndov 18895 | . . . . . . . . 9
⊢ ((𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝑥(+g‘𝑀)𝑦) = (𝑥 ∘ 𝑦)) | 
| 33 | 30, 32 | syl 17 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥:𝐴–1-1→𝐴 ∧ 𝑦:𝐴–1-1→𝐴)) → (𝑥(+g‘𝑀)𝑦) = (𝑥 ∘ 𝑦)) | 
| 34 | 33 | eleq1d 2825 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥:𝐴–1-1→𝐴 ∧ 𝑦:𝐴–1-1→𝐴)) → ((𝑥(+g‘𝑀)𝑦) ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴} ↔ (𝑥 ∘ 𝑦) ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴})) | 
| 35 | 1, 19 | coex 7953 | . . . . . . . 8
⊢ (𝑥 ∘ 𝑦) ∈ V | 
| 36 |  | f1eq1 6798 | . . . . . . . 8
⊢ (ℎ = (𝑥 ∘ 𝑦) → (ℎ:𝐴–1-1→𝐴 ↔ (𝑥 ∘ 𝑦):𝐴–1-1→𝐴)) | 
| 37 | 35, 36 | elab 3678 | . . . . . . 7
⊢ ((𝑥 ∘ 𝑦) ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴} ↔ (𝑥 ∘ 𝑦):𝐴–1-1→𝐴) | 
| 38 | 34, 37 | bitrdi 287 | . . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥:𝐴–1-1→𝐴 ∧ 𝑦:𝐴–1-1→𝐴)) → ((𝑥(+g‘𝑀)𝑦) ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴} ↔ (𝑥 ∘ 𝑦):𝐴–1-1→𝐴)) | 
| 39 | 24, 38 | mpbird 257 | . . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥:𝐴–1-1→𝐴 ∧ 𝑦:𝐴–1-1→𝐴)) → (𝑥(+g‘𝑀)𝑦) ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴}) | 
| 40 | 39 | ex 412 | . . . 4
⊢ (𝐴 ∈ 𝑉 → ((𝑥:𝐴–1-1→𝐴 ∧ 𝑦:𝐴–1-1→𝐴) → (𝑥(+g‘𝑀)𝑦) ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴})) | 
| 41 | 22, 40 | biimtrid 242 | . . 3
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴} ∧ 𝑦 ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴}) → (𝑥(+g‘𝑀)𝑦) ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴})) | 
| 42 | 41 | ralrimivv 3199 | . 2
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴}∀𝑦 ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴} (𝑥(+g‘𝑀)𝑦) ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴}) | 
| 43 | 5 | efmndmnd 18903 | . . 3
⊢ (𝐴 ∈ 𝑉 → 𝑀 ∈ Mnd) | 
| 44 |  | eqid 2736 | . . . 4
⊢
(0g‘𝑀) = (0g‘𝑀) | 
| 45 | 6, 44, 31 | issubm 18817 | . . 3
⊢ (𝑀 ∈ Mnd → ({ℎ ∣ ℎ:𝐴–1-1→𝐴} ∈ (SubMnd‘𝑀) ↔ ({ℎ ∣ ℎ:𝐴–1-1→𝐴} ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴} ∧ ∀𝑥 ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴}∀𝑦 ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴} (𝑥(+g‘𝑀)𝑦) ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴}))) | 
| 46 | 43, 45 | syl 17 | . 2
⊢ (𝐴 ∈ 𝑉 → ({ℎ ∣ ℎ:𝐴–1-1→𝐴} ∈ (SubMnd‘𝑀) ↔ ({ℎ ∣ ℎ:𝐴–1-1→𝐴} ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴} ∧ ∀𝑥 ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴}∀𝑦 ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴} (𝑥(+g‘𝑀)𝑦) ∈ {ℎ ∣ ℎ:𝐴–1-1→𝐴}))) | 
| 47 | 10, 18, 42, 46 | mpbir3and 1342 | 1
⊢ (𝐴 ∈ 𝑉 → {ℎ ∣ ℎ:𝐴–1-1→𝐴} ∈ (SubMnd‘𝑀)) |