Metamath Proof Explorer


Theorem efgmnvl

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

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

Proof

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