Metamath Proof Explorer


Theorem ring1

Description: The (smallest) structure representing azero ring. (Contributed by AV, 28-Apr-2019)

Ref Expression
Hypothesis ring1.m 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ }
Assertion ring1 ( 𝑍𝑉𝑀 ∈ Ring )

Proof

Step Hyp Ref Expression
1 ring1.m 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ }
2 eqid { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ } = { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ }
3 2 grp1 ( 𝑍𝑉 → { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ } ∈ Grp )
4 snex { 𝑍 } ∈ V
5 1 rngbase ( { 𝑍 } ∈ V → { 𝑍 } = ( Base ‘ 𝑀 ) )
6 4 5 ax-mp { 𝑍 } = ( Base ‘ 𝑀 )
7 6 eqcomi ( Base ‘ 𝑀 ) = { 𝑍 }
8 snex { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∈ V
9 1 rngplusg ( { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∈ V → { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } = ( +g𝑀 ) )
10 9 eqcomd ( { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∈ V → ( +g𝑀 ) = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } )
11 8 10 ax-mp ( +g𝑀 ) = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ }
12 7 11 2 grppropstr ( 𝑀 ∈ Grp ↔ { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ } ∈ Grp )
13 3 12 sylibr ( 𝑍𝑉𝑀 ∈ Grp )
14 2 mnd1 ( 𝑍𝑉 → { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ } ∈ Mnd )
15 eqid ( mulGrp ‘ 𝑀 ) = ( mulGrp ‘ 𝑀 )
16 15 6 mgpbas { 𝑍 } = ( Base ‘ ( mulGrp ‘ 𝑀 ) )
17 2 grpbase ( { 𝑍 } ∈ V → { 𝑍 } = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ } ) )
18 4 17 ax-mp { 𝑍 } = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ } )
19 16 18 eqtr3i ( Base ‘ ( mulGrp ‘ 𝑀 ) ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ } )
20 1 rngmulr ( { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∈ V → { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } = ( .r𝑀 ) )
21 8 20 ax-mp { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } = ( .r𝑀 )
22 2 grpplusg ( { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∈ V → { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } = ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ } ) )
23 8 22 ax-mp { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } = ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ } )
24 eqid ( .r𝑀 ) = ( .r𝑀 )
25 15 24 mgpplusg ( .r𝑀 ) = ( +g ‘ ( mulGrp ‘ 𝑀 ) )
26 21 23 25 3eqtr3ri ( +g ‘ ( mulGrp ‘ 𝑀 ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ } )
27 19 26 mndprop ( ( mulGrp ‘ 𝑀 ) ∈ Mnd ↔ { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ } ∈ Mnd )
28 14 27 sylibr ( 𝑍𝑉 → ( mulGrp ‘ 𝑀 ) ∈ Mnd )
29 df-ov ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) = ( { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ‘ ⟨ 𝑍 , 𝑍 ⟩ )
30 opex 𝑍 , 𝑍 ⟩ ∈ V
31 fvsng ( ( ⟨ 𝑍 , 𝑍 ⟩ ∈ V ∧ 𝑍𝑉 ) → ( { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ‘ ⟨ 𝑍 , 𝑍 ⟩ ) = 𝑍 )
32 30 31 mpan ( 𝑍𝑉 → ( { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ‘ ⟨ 𝑍 , 𝑍 ⟩ ) = 𝑍 )
33 29 32 eqtrid ( 𝑍𝑉 → ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) = 𝑍 )
34 33 oveq2d ( 𝑍𝑉 → ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) = ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) )
35 33 33 oveq12d ( 𝑍𝑉 → ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) = ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) )
36 34 35 eqtr4d ( 𝑍𝑉 → ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) )
37 33 oveq1d ( 𝑍𝑉 → ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) = ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) )
38 37 35 eqtr4d ( 𝑍𝑉 → ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) )
39 oveq1 ( 𝑎 = 𝑍 → ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) )
40 oveq1 ( 𝑎 = 𝑍 → ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) = ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) )
41 oveq1 ( 𝑎 = 𝑍 → ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) )
42 40 41 oveq12d ( 𝑎 = 𝑍 → ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) )
43 39 42 eqeq12d ( 𝑎 = 𝑍 → ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ↔ ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) )
44 40 oveq1d ( 𝑎 = 𝑍 → ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) )
45 41 oveq1d ( 𝑎 = 𝑍 → ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) )
46 44 45 eqeq12d ( 𝑎 = 𝑍 → ( ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ↔ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) )
47 43 46 anbi12d ( 𝑎 = 𝑍 → ( ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ↔ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ) )
48 47 2ralbidv ( 𝑎 = 𝑍 → ( ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ↔ ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ) )
49 48 ralsng ( 𝑍𝑉 → ( ∀ 𝑎 ∈ { 𝑍 } ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ↔ ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ) )
50 oveq1 ( 𝑏 = 𝑍 → ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) )
51 50 oveq2d ( 𝑏 = 𝑍 → ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) )
52 oveq2 ( 𝑏 = 𝑍 → ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) = ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) )
53 52 oveq1d ( 𝑏 = 𝑍 → ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) )
54 51 53 eqeq12d ( 𝑏 = 𝑍 → ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ↔ ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) )
55 52 oveq1d ( 𝑏 = 𝑍 → ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) )
56 50 oveq2d ( 𝑏 = 𝑍 → ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) )
57 55 56 eqeq12d ( 𝑏 = 𝑍 → ( ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ↔ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) )
58 54 57 anbi12d ( 𝑏 = 𝑍 → ( ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ↔ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ) )
59 58 ralbidv ( 𝑏 = 𝑍 → ( ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ↔ ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ) )
60 59 ralsng ( 𝑍𝑉 → ( ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ↔ ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ) )
61 oveq2 ( 𝑐 = 𝑍 → ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) )
62 61 oveq2d ( 𝑐 = 𝑍 → ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) )
63 61 oveq2d ( 𝑐 = 𝑍 → ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) )
64 62 63 eqeq12d ( 𝑐 = 𝑍 → ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ↔ ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) ) )
65 oveq2 ( 𝑐 = 𝑍 → ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) )
66 61 61 oveq12d ( 𝑐 = 𝑍 → ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) )
67 65 66 eqeq12d ( 𝑐 = 𝑍 → ( ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ↔ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) ) )
68 64 67 anbi12d ( 𝑐 = 𝑍 → ( ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ↔ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) ∧ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) ) ) )
69 68 ralsng ( 𝑍𝑉 → ( ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ↔ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) ∧ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) ) ) )
70 49 60 69 3bitrd ( 𝑍𝑉 → ( ∀ 𝑎 ∈ { 𝑍 } ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ↔ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) ∧ ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) = ( ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑍 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑍 ) ) ) ) )
71 36 38 70 mpbir2and ( 𝑍𝑉 → ∀ 𝑎 ∈ { 𝑍 } ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) )
72 8 9 ax-mp { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } = ( +g𝑀 )
73 6 15 72 21 isring ( 𝑀 ∈ Ring ↔ ( 𝑀 ∈ Grp ∧ ( mulGrp ‘ 𝑀 ) ∈ Mnd ∧ ∀ 𝑎 ∈ { 𝑍 } ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) = ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ∧ ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑏 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) = ( ( 𝑎 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ( 𝑏 { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } 𝑐 ) ) ) ) )
74 13 28 71 73 syl3anbrc ( 𝑍𝑉𝑀 ∈ Ring )