Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-isom Unicode version

Definition df-isom 4941
 Description: Define the isomorphism predicate. We read this as " is an , isomorphism of onto ." Normally, and are ordering relations on and respectively. Definition 6.28 of [TakeutiZaring] p. 32, whose notation is the same as ours except that and are subscripts. (Contributed by NM, 4-Mar-1997.)
Assertion
Ref Expression
df-isom
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,

Detailed syntax breakdown of Definition df-isom
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cR . . 3
4 cS . . 3
5 cH . . 3
61, 2, 3, 4, 5wiso 4933 . 2
71, 2, 5wf1o 4931 . . 3
8 vx . . . . . . . 8
98cv 1284 . . . . . . 7
10 vy . . . . . . . 8
1110cv 1284 . . . . . . 7
129, 11, 3wbr 3793 . . . . . 6
139, 5cfv 4932 . . . . . . 7
1411, 5cfv 4932 . . . . . . 7
1513, 14, 4wbr 3793 . . . . . 6
1612, 15wb 103 . . . . 5
1716, 10, 1wral 2349 . . . 4
1817, 8, 1wral 2349 . . 3
197, 18wa 102 . 2
206, 19wb 103 1
 Colors of variables: wff set class This definition is referenced by:  isoeq1  5472  isoeq2  5473  isoeq3  5474  isoeq4  5475  isoeq5  5476  nfiso  5477  isof1o  5478  isorel  5479  isoid  5481  isocnv  5482  isocnv2  5483  isores2  5484  isores3  5486  isotr  5487  isoini2  5489  f1oiso  5496  negiso  8100  frec2uzisod  9489
 Copyright terms: Public domain W3C validator