This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grposnOLD

Description: The group operation for the singleton group. Obsolete, use grp1 . instead. (Contributed by NM, 4-Nov-2006) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis grposnOLD.1 ⊢ 𝐴 ∈ V
Assertion grposnOLD { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∈ GrpOp

Proof

Step Hyp Ref Expression
1 grposnOLD.1 ⊢ 𝐴 ∈ V
2 snex ⊢ { 𝐴 } ∈ V
3 opex ⊢ ⟨ 𝐴 , 𝐴 ⟩ ∈ V
4 3 1 f1osn ⊢ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } : { ⟨ 𝐴 , 𝐴 ⟩ } –1-1-onto→ { 𝐴 }
5 f1of ⊢ ( { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } : { ⟨ 𝐴 , 𝐴 ⟩ } –1-1-onto→ { 𝐴 } → { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } : { ⟨ 𝐴 , 𝐴 ⟩ } ⟶ { 𝐴 } )
6 4 5 ax-mp ⊢ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } : { ⟨ 𝐴 , 𝐴 ⟩ } ⟶ { 𝐴 }
7 1 1 xpsn ⊢ ( { 𝐴 } × { 𝐴 } ) = { ⟨ 𝐴 , 𝐴 ⟩ }
8 7 feq2i ⊢ ( { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } : ( { 𝐴 } × { 𝐴 } ) ⟶ { 𝐴 } ↔ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } : { ⟨ 𝐴 , 𝐴 ⟩ } ⟶ { 𝐴 } )
9 6 8 mpbir ⊢ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } : ( { 𝐴 } × { 𝐴 } ) ⟶ { 𝐴 }
10 velsn ⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
11 velsn ⊢ ( 𝑦 ∈ { 𝐴 } ↔ 𝑦 = 𝐴 )
12 velsn ⊢ ( 𝑧 ∈ { 𝐴 } ↔ 𝑧 = 𝐴 )
13 oveq2 ⊢ ( 𝑧 = 𝐴 → ( ( 𝑥 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) = ( ( 𝑥 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝐴 ) )
14 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑦 ) = ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑦 ) )
15 oveq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑦 ) = ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝐴 ) )
16 df-ov ⊢ ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝐴 ) = ( { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ‘ ⟨ 𝐴 , 𝐴 ⟩ )
17 3 1 fvsn ⊢ ( { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ‘ ⟨ 𝐴 , 𝐴 ⟩ ) = 𝐴
18 16 17 eqtri ⊢ ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝐴 ) = 𝐴
19 15 18 eqtrdi ⊢ ( 𝑦 = 𝐴 → ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑦 ) = 𝐴 )
20 14 19 sylan9eq ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) → ( 𝑥 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑦 ) = 𝐴 )
21 20 oveq1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) → ( ( 𝑥 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝐴 ) = ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝐴 ) )
22 21 18 eqtrdi ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) → ( ( 𝑥 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝐴 ) = 𝐴 )
23 13 22 sylan9eqr ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) ∧ 𝑧 = 𝐴 ) → ( ( 𝑥 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) = 𝐴 )
24 23 3impa ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ∧ 𝑧 = 𝐴 ) → ( ( 𝑥 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) = 𝐴 )
25 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) ) = ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) ) )
26 oveq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) = ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) )
27 oveq2 ⊢ ( 𝑧 = 𝐴 → ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) = ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝐴 ) )
28 27 18 eqtrdi ⊢ ( 𝑧 = 𝐴 → ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) = 𝐴 )
29 26 28 sylan9eq ⊢ ( ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐴 ) → ( 𝑦 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) = 𝐴 )
30 29 oveq2d ⊢ ( ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐴 ) → ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) ) = ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝐴 ) )
31 30 18 eqtrdi ⊢ ( ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐴 ) → ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) ) = 𝐴 )
32 25 31 sylan9eq ⊢ ( ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐴 ) ) → ( 𝑥 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) ) = 𝐴 )
33 32 3impb ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ∧ 𝑧 = 𝐴 ) → ( 𝑥 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) ) = 𝐴 )
34 24 33 eqtr4d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ∧ 𝑧 = 𝐴 ) → ( ( 𝑥 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) = ( 𝑥 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) ) )
35 10 11 12 34 syl3anb ⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ∧ 𝑧 ∈ { 𝐴 } ) → ( ( 𝑥 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑦 ) { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) = ( 𝑥 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ( 𝑦 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑧 ) ) )
36 1 snid ⊢ 𝐴 ∈ { 𝐴 }
37 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑥 ) = ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝐴 ) )
38 37 18 eqtrdi ⊢ ( 𝑥 = 𝐴 → ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑥 ) = 𝐴 )
39 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
40 38 39 eqtr4d ⊢ ( 𝑥 = 𝐴 → ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑥 ) = 𝑥 )
41 10 40 sylbi ⊢ ( 𝑥 ∈ { 𝐴 } → ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑥 ) = 𝑥 )
42 36 a1i ⊢ ( 𝑥 ∈ { 𝐴 } → 𝐴 ∈ { 𝐴 } )
43 10 38 sylbi ⊢ ( 𝑥 ∈ { 𝐴 } → ( 𝐴 { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } 𝑥 ) = 𝐴 )
44 2 9 35 36 41 42 43 isgrpoi ⊢ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∈ GrpOp