Metamath Proof Explorer

Theorem efgmf

Description: The formal inverse operation is an endofunction on the generating set. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypothesis efgmval.m ${⊢}{M}=\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)$
Assertion efgmf ${⊢}{M}:{I}×{2}_{𝑜}⟶{I}×{2}_{𝑜}$

Proof

Step Hyp Ref Expression
1 efgmval.m ${⊢}{M}=\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)$
2 2oconcl ${⊢}{z}\in {2}_{𝑜}\to {1}_{𝑜}\setminus {z}\in {2}_{𝑜}$
3 opelxpi ${⊢}\left({y}\in {I}\wedge {1}_{𝑜}\setminus {z}\in {2}_{𝑜}\right)\to ⟨{y},{1}_{𝑜}\setminus {z}⟩\in \left({I}×{2}_{𝑜}\right)$
4 2 3 sylan2 ${⊢}\left({y}\in {I}\wedge {z}\in {2}_{𝑜}\right)\to ⟨{y},{1}_{𝑜}\setminus {z}⟩\in \left({I}×{2}_{𝑜}\right)$
5 4 rgen2 ${⊢}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}⟨{y},{1}_{𝑜}\setminus {z}⟩\in \left({I}×{2}_{𝑜}\right)$
6 1 fmpo ${⊢}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {z}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}⟨{y},{1}_{𝑜}\setminus {z}⟩\in \left({I}×{2}_{𝑜}\right)↔{M}:{I}×{2}_{𝑜}⟶{I}×{2}_{𝑜}$
7 5 6 mpbi ${⊢}{M}:{I}×{2}_{𝑜}⟶{I}×{2}_{𝑜}$