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=BaseM
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=BaseM
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