Metamath Proof Explorer

Theorem rabsubmgmd

Description: Deduction for proving that a restricted class abstraction is a submagma. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypotheses rabsubmgmd.b ⊢ B = Base M
rabsubmgmd.p ⊢ + ˙ = + M
rabsubmgmd.m ⊢ φ → M ∈ Mgm
rabsubmgmd.cp ⊢ φ ∧ x ∈ B ∧ y ∈ B ∧ θ ∧ τ → η
rabsubmgmd.th ⊢ z = x → ψ ↔ θ
rabsubmgmd.ta ⊢ z = y → ψ ↔ τ
rabsubmgmd.et ⊢ z = x + ˙ y → ψ ↔ η
Assertion rabsubmgmd ⊢ φ → z ∈ B | ψ ∈ SubMgm ⁡ M

Proof

Step Hyp Ref Expression
1 rabsubmgmd.b ⊢ B = Base M
2 rabsubmgmd.p ⊢ + ˙ = + M
3 rabsubmgmd.m ⊢ φ → M ∈ Mgm
4 rabsubmgmd.cp ⊢ φ ∧ x ∈ B ∧ y ∈ B ∧ θ ∧ τ → η
5 rabsubmgmd.th ⊢ z = x → ψ ↔ θ
6 rabsubmgmd.ta ⊢ z = y → ψ ↔ τ
7 rabsubmgmd.et ⊢ z = x + ˙ y → ψ ↔ η
8 ssrab2 ⊢ z ∈ B | ψ ⊆ B
9 8 a1i ⊢ φ → z ∈ B | ψ ⊆ B
10 5 elrab ⊢ x ∈ z ∈ B | ψ ↔ x ∈ B ∧ θ
11 6 elrab ⊢ y ∈ z ∈ B | ψ ↔ y ∈ B ∧ τ
12 10 11 anbi12i ⊢ x ∈ z ∈ B | ψ ∧ y ∈ z ∈ B | ψ ↔ x ∈ B ∧ θ ∧ y ∈ B ∧ τ
13 3 adantr ⊢ φ ∧ x ∈ B ∧ θ ∧ y ∈ B ∧ τ → M ∈ Mgm
14 simprll ⊢ φ ∧ x ∈ B ∧ θ ∧ y ∈ B ∧ τ → x ∈ B
15 simprrl ⊢ φ ∧ x ∈ B ∧ θ ∧ y ∈ B ∧ τ → y ∈ B
16 1 2 mgmcl ⊢ M ∈ Mgm ∧ x ∈ B ∧ y ∈ B → x + ˙ y ∈ B
17 13 14 15 16 syl3anc ⊢ φ ∧ x ∈ B ∧ θ ∧ y ∈ B ∧ τ → x + ˙ y ∈ B
18 simpl ⊢ x ∈ B ∧ θ → x ∈ B
19 simpl ⊢ y ∈ B ∧ τ → y ∈ B
20 18 19 anim12i ⊢ x ∈ B ∧ θ ∧ y ∈ B ∧ τ → x ∈ B ∧ y ∈ B
21 simpr ⊢ x ∈ B ∧ θ → θ
22 simpr ⊢ y ∈ B ∧ τ → τ
23 21 22 anim12i ⊢ x ∈ B ∧ θ ∧ y ∈ B ∧ τ → θ ∧ τ
24 20 23 jca ⊢ x ∈ B ∧ θ ∧ y ∈ B ∧ τ → x ∈ B ∧ y ∈ B ∧ θ ∧ τ
25 24 4 sylan2 ⊢ φ ∧ x ∈ B ∧ θ ∧ y ∈ B ∧ τ → η
26 7 17 25 elrabd ⊢ φ ∧ x ∈ B ∧ θ ∧ y ∈ B ∧ τ → x + ˙ y ∈ z ∈ B | ψ
27 12 26 sylan2b ⊢ φ ∧ x ∈ z ∈ B | ψ ∧ y ∈ z ∈ B | ψ → x + ˙ y ∈ z ∈ B | ψ
28 27 ralrimivva ⊢ φ → ∀ x ∈ z ∈ B | ψ ∀ y ∈ z ∈ B | ψ x + ˙ y ∈ z ∈ B | ψ
29 1 2 issubmgm ⊢ M ∈ Mgm → z ∈ B | ψ ∈ SubMgm ⁡ M ↔ z ∈ B | ψ ⊆ B ∧ ∀ x ∈ z ∈ B | ψ ∀ y ∈ z ∈ B | ψ x + ˙ y ∈ z ∈ B | ψ
30 3 29 syl ⊢ φ → z ∈ B | ψ ∈ SubMgm ⁡ M ↔ z ∈ B | ψ ⊆ B ∧ ∀ x ∈ z ∈ B | ψ ∀ y ∈ z ∈ B | ψ x + ˙ y ∈ z ∈ B | ψ
31 9 28 30 mpbir2and ⊢ φ → z ∈ B | ψ ∈ SubMgm ⁡ M