efgmnvl

Description: The inversion function on the generators is an involution. (Contributed by Mario Carneiro, 1-Oct-2015)

		Ref	Expression
	Hypothesis	efgmval.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ )
	Assertion	efgmnvl	⊢ ( 𝐴 ∈ ( 𝐼 × 2_o ) → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		efgmval.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ )
2		elxp2	⊢ ( 𝐴 ∈ ( 𝐼 × 2_o ) ↔ ∃ 𝑎 ∈ 𝐼 ∃ 𝑏 ∈ 2_o 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ )
3	1	efgmval	⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) → ( 𝑎 𝑀 𝑏 ) = ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ )
4	3	fveq2d	⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) → ( 𝑀 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑀 ‘ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ) )
5		df-ov	⊢ ( 𝑎 𝑀 ( 1_o ∖ 𝑏 ) ) = ( 𝑀 ‘ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ )
6	4 5	eqtr4di	⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) → ( 𝑀 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑎 𝑀 ( 1_o ∖ 𝑏 ) ) )
7		2oconcl	⊢ ( 𝑏 ∈ 2_o → ( 1_o ∖ 𝑏 ) ∈ 2_o )
8	1	efgmval	⊢ ( ( 𝑎 ∈ 𝐼 ∧ ( 1_o ∖ 𝑏 ) ∈ 2_o ) → ( 𝑎 𝑀 ( 1_o ∖ 𝑏 ) ) = ⟨ 𝑎 , ( 1_o ∖ ( 1_o ∖ 𝑏 ) ) ⟩ )
9	7 8	sylan2	⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) → ( 𝑎 𝑀 ( 1_o ∖ 𝑏 ) ) = ⟨ 𝑎 , ( 1_o ∖ ( 1_o ∖ 𝑏 ) ) ⟩ )
10		1on	⊢ 1_o ∈ On
11	10	onordi	⊢ Ord 1_o
12		ordtr	⊢ ( Ord 1_o → Tr 1_o )
13		trsucss	⊢ ( Tr 1_o → ( 𝑏 ∈ suc 1_o → 𝑏 ⊆ 1_o ) )
14	11 12 13	mp2b	⊢ ( 𝑏 ∈ suc 1_o → 𝑏 ⊆ 1_o )
15		df-2o	⊢ 2_o = suc 1_o
16	14 15	eleq2s	⊢ ( 𝑏 ∈ 2_o → 𝑏 ⊆ 1_o )
17	16	adantl	⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) → 𝑏 ⊆ 1_o )
18		dfss4	⊢ ( 𝑏 ⊆ 1_o ↔ ( 1_o ∖ ( 1_o ∖ 𝑏 ) ) = 𝑏 )
19	17 18	sylib	⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) → ( 1_o ∖ ( 1_o ∖ 𝑏 ) ) = 𝑏 )
20	19	opeq2d	⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) → ⟨ 𝑎 , ( 1_o ∖ ( 1_o ∖ 𝑏 ) ) ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
21	6 9 20	3eqtrd	⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) → ( 𝑀 ‘ ( 𝑎 𝑀 𝑏 ) ) = ⟨ 𝑎 , 𝑏 ⟩ )
22		fveq2	⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀 ‘ 𝐴 ) = ( 𝑀 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
23		df-ov	⊢ ( 𝑎 𝑀 𝑏 ) = ( 𝑀 ‘ ⟨ 𝑎 , 𝑏 ⟩ )
24	22 23	eqtr4di	⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀 ‘ 𝐴 ) = ( 𝑎 𝑀 𝑏 ) )
25	24	fveq2d	⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑎 𝑀 𝑏 ) ) )
26		id	⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ )
27	25 26	eqeq12d	⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ↔ ( 𝑀 ‘ ( 𝑎 𝑀 𝑏 ) ) = ⟨ 𝑎 , 𝑏 ⟩ ) )
28	21 27	syl5ibrcom	⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) → ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) )
29	28	rexlimivv	⊢ ( ∃ 𝑎 ∈ 𝐼 ∃ 𝑏 ∈ 2_o 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 )
30	2 29	sylbi	⊢ ( 𝐴 ∈ ( 𝐼 × 2_o ) → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 )

Metamath Proof Explorer

Theorem efgmnvl

Proof