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

Definition df-iso 4796
Description: Define the isomorphism predicate. We read this as "H is an R, S isomorphism of A onto B." Normally, R and S are ordering relations on A and B respectively. Definition 6.28 of [TakeutiZaring] p. 32, whose notation is the same as ours except that R and S are subscripts. (Contributed by SF, 5-Jan-2015.)
Assertion
Ref Expression
df-iso (H Isom R, S (A, B) ↔ (H:A1-1-ontoB x A y A (xRy ↔ (Hx)S(Hy))))
Distinct variable groups:   x,y,A   x,B,y   x,R,y   x,S,y   x,H,y

Detailed syntax breakdown of Definition df-iso
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
3 cR . . 3 class R
4 cS . . 3 class S
5 cH . . 3 class H
61, 2, 3, 4, 5wiso 4782 . 2 wff H Isom R, S (A, B)
71, 2, 5wf1o 4780 . . 3 wff H:A1-1-ontoB
8 vx . . . . . . . 8 setvar x
98cv 1641 . . . . . . 7 class x
10 vy . . . . . . . 8 setvar y
1110cv 1641 . . . . . . 7 class y
129, 11, 3wbr 4639 . . . . . 6 wff xRy
139, 5cfv 4781 . . . . . . 7 class (Hx)
1411, 5cfv 4781 . . . . . . 7 class (Hy)
1513, 14, 4wbr 4639 . . . . . 6 wff (Hx)S(Hy)
1612, 15wb 176 . . . . 5 wff (xRy ↔ (Hx)S(Hy))
1716, 10, 1wral 2614 . . . 4 wff y A (xRy ↔ (Hx)S(Hy))
1817, 8, 1wral 2614 . . 3 wff x A y A (xRy ↔ (Hx)S(Hy))
197, 18wa 358 . 2 wff (H:A1-1-ontoB x A y A (xRy ↔ (Hx)S(Hy)))
206, 19wb 176 1 wff (H Isom R, S (A, B) ↔ (H:A1-1-ontoB x A y A (xRy ↔ (Hx)S(Hy))))
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