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

Definition df-isom 5140
 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 5132 . 2
71, 2, 5wf1o 5130 . . 3
8 vx . . . . . . . 8
98cv 1331 . . . . . . 7
10 vy . . . . . . . 8
1110cv 1331 . . . . . . 7
129, 11, 3wbr 3937 . . . . . 6
139, 5cfv 5131 . . . . . . 7
1411, 5cfv 5131 . . . . . . 7
1513, 14, 4wbr 3937 . . . . . 6
1612, 15wb 104 . . . . 5
1716, 10, 1wral 2417 . . . 4
1817, 8, 1wral 2417 . . 3
197, 18wa 103 . 2
206, 19wb 104 1
 Colors of variables: wff set class This definition is referenced by:  isoeq1  5710  isoeq2  5711  isoeq3  5712  isoeq4  5713  isoeq5  5714  nfiso  5715  isof1o  5716  isorel  5717  isoid  5719  isocnv  5720  isocnv2  5721  isores2  5722  isores3  5724  isotr  5725  iso0  5726  isoini2  5728  f1oiso  5735  negiso  8737  frec2uzisod  10211  zfz1isolem1  10615  xrnegiso  11063  reefiso  12906  logltb  13003
 Copyright terms: Public domain W3C validator