New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-iso Unicode version

Definition df-iso 4796
 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 SF, 5-Jan-2015.)
Assertion
Ref Expression
df-iso
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,

Detailed syntax breakdown of Definition df-iso
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cR . . 3
4 cS . . 3
5 cH . . 3
61, 2, 3, 4, 5wiso 4782 . 2
71, 2, 5wf1o 4780 . . 3
8 vx . . . . . . . 8
98cv 1641 . . . . . . 7
10 vy . . . . . . . 8
1110cv 1641 . . . . . . 7
129, 11, 3wbr 4639 . . . . . 6
139, 5cfv 4781 . . . . . . 7
1411, 5cfv 4781 . . . . . . 7
1513, 14, 4wbr 4639 . . . . . 6
1612, 15wb 176 . . . . 5
1716, 10, 1wral 2614 . . . 4
1817, 8, 1wral 2614 . . 3
197, 18wa 358 . 2
206, 19wb 176 1
 Colors of variables: wff setvar class This definition is referenced by:  isoeq1  5482  isoeq2  5483  isoeq3  5484  isoeq4  5485  isoeq5  5486  nfiso  5487  isof1o  5488  isorel  5489  isoid  5490  isocnv  5491  isocnv2  5492  isores2  5493  isotr  5495  isoini2  5498  f1oiso  5499
 Copyright terms: Public domain W3C validator