Definition df-ismt 25428

Description: Define the set of isometries between two structures. Definition 4.8 of [Schwabhauser] p. 36. See isismt 25429. (Contributed by Thierry Arnoux, 13-Dec-2019.)

Assertion

Ref	Expression
df-ismt	|- Ismt = ( g e. _V , h e. _V |-> { f | ( f : ( Base ` g ) -1-1-onto-> ( Base ` h ) /\ A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b ) ) } )

Distinct variable group:   a, b, f, g, h

Detailed syntax breakdown of Definition df-ismt

Step	Hyp	Ref	Expression
1		cismt 25427	. 2 class Ismt
2		vg	. . 3 setvar g
3		vh	. . 3 setvar h
4		cvv 3200	. . 3 class _V
5	2	cv 1482	. . . . . . 7 class g
6		cbs 15857	. . . . . . 7 class Base
7	5, 6	cfv 5888	. . . . . 6 class ( Base ` g )
8	3	cv 1482	. . . . . . 7 class h
9	8, 6	cfv 5888	. . . . . 6 class ( Base ` h )
10		vf	. . . . . . 7 setvar f
11	10	cv 1482	. . . . . 6 class f
12	7, 9, 11	wf1o 5887	. . . . 5 wff f : ( Base ` g ) -1-1-onto-> ( Base ` h )
13		va	. . . . . . . . . . 11 setvar a
14	13	cv 1482	. . . . . . . . . 10 class a
15	14, 11	cfv 5888	. . . . . . . . 9 class ( f ` a )
16		vb	. . . . . . . . . . 11 setvar b
17	16	cv 1482	. . . . . . . . . 10 class b
18	17, 11	cfv 5888	. . . . . . . . 9 class ( f ` b )
19		cds 15950	. . . . . . . . . 10 class dist
20	8, 19	cfv 5888	. . . . . . . . 9 class ( dist ` h )
21	15, 18, 20	co 6650	. . . . . . . 8 class ( ( f ` a ) ( dist ` h ) ( f ` b ) )
22	5, 19	cfv 5888	. . . . . . . . 9 class ( dist ` g )
23	14, 17, 22	co 6650	. . . . . . . 8 class ( a ( dist ` g ) b )
24	21, 23	wceq 1483	. . . . . . 7 wff ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b )
25	24, 16, 7	wral 2912	. . . . . 6 wff A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b )
26	25, 13, 7	wral 2912	. . . . 5 wff A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b )
27	12, 26	wa 384	. . . 4 wff ( f : ( Base ` g ) -1-1-onto-> ( Base ` h ) /\ A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b ) )
28	27, 10	cab 2608	. . 3 class { f | ( f : ( Base ` g ) -1-1-onto-> ( Base ` h ) /\ A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b ) ) }
29	2, 3, 4, 4, 28	cmpt2 6652	. 2 class ( g e. _V , h e. _V |-> { f | ( f : ( Base ` g ) -1-1-onto-> ( Base ` h ) /\ A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b ) ) } )
30	1, 29	wceq 1483	1 wff Ismt = ( g e. _V , h e. _V |-> { f | ( f : ( Base ` g ) -1-1-onto-> ( Base ` h ) /\ A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b ) ) } )

This definition is referenced by:  isismt  25429