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	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
Assertion	efgmf	⊢ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o )

Proof

Step	Hyp	Ref	Expression
1		efgmval.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
2		2oconcl	⊢ ( 𝑧 ∈ 2o → ( 1o ∖ 𝑧 ) ∈ 2o )
3		opelxpi	⊢ ( ( 𝑦 ∈ 𝐼 ∧ ( 1o ∖ 𝑧 ) ∈ 2o ) → ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ∈ ( 𝐼 × 2o ) )
4	2 3	sylan2	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o ) → ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ∈ ( 𝐼 × 2o ) )
5	4	rgen2	⊢ ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ∈ ( 𝐼 × 2o )
6	1	fmpo	⊢ ( ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ∈ ( 𝐼 × 2o ) ↔ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o ) )
7	5 6	mpbi	⊢ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o )