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

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 )