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