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

Definition df-isom 4854
Description: Define the isomorphism predicate. We read this as "𝐻 is an 𝑅, 𝑆 isomorphism of A onto B." Normally, 𝑅 and 𝑆 are ordering relations on A and B 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 (𝐻 Isom 𝑅, 𝑆 (A, B) ↔ (𝐻:A1-1-ontoB x A y A (x𝑅y ↔ (𝐻x)𝑆(𝐻y))))
Distinct variable groups:   x,y,A   x,B,y   x,𝑅,y   x,𝑆,y   x,𝐻,y

Detailed syntax breakdown of Definition df-isom
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
3 cR . . 3 class 𝑅
4 cS . . 3 class 𝑆
5 cH . . 3 class 𝐻
61, 2, 3, 4, 5wiso 4846 . 2 wff 𝐻 Isom 𝑅, 𝑆 (A, B)
71, 2, 5wf1o 4844 . . 3 wff 𝐻:A1-1-ontoB
8 vx . . . . . . . 8 setvar x
98cv 1241 . . . . . . 7 class x
10 vy . . . . . . . 8 setvar y
1110cv 1241 . . . . . . 7 class y
129, 11, 3wbr 3755 . . . . . 6 wff x𝑅y
139, 5cfv 4845 . . . . . . 7 class (𝐻x)
1411, 5cfv 4845 . . . . . . 7 class (𝐻y)
1513, 14, 4wbr 3755 . . . . . 6 wff (𝐻x)𝑆(𝐻y)
1612, 15wb 98 . . . . 5 wff (x𝑅y ↔ (𝐻x)𝑆(𝐻y))
1716, 10, 1wral 2300 . . . 4 wff y A (x𝑅y ↔ (𝐻x)𝑆(𝐻y))
1817, 8, 1wral 2300 . . 3 wff x A y A (x𝑅y ↔ (𝐻x)𝑆(𝐻y))
197, 18wa 97 . 2 wff (𝐻:A1-1-ontoB x A y A (x𝑅y ↔ (𝐻x)𝑆(𝐻y)))
206, 19wb 98 1 wff (𝐻 Isom 𝑅, 𝑆 (A, B) ↔ (𝐻:A1-1-ontoB x A y A (x𝑅y ↔ (𝐻x)𝑆(𝐻y))))
Colors of variables: wff set class
This definition is referenced by:  isoeq1  5384  isoeq2  5385  isoeq3  5386  isoeq4  5387  isoeq5  5388  nfiso  5389  isof1o  5390  isorel  5391  isoid  5393  isocnv  5394  isocnv2  5395  isores2  5396  isores3  5398  isotr  5399  isoini2  5401  f1oiso  5408  frec2uzisod  8854
  Copyright terms: Public domain W3C validator