Definition df-isom 6427

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	⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦   𝑥,𝐻,𝑦

Detailed syntax breakdown of Definition df-isom

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cR	. . 3 class 𝑅
4		cS	. . 3 class 𝑆
5		cH	. . 3 class 𝐻
6	1, 2, 3, 4, 5	wiso 6419	. 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
7	1, 2, 5	wf1o 6417	. . 3 wff 𝐻:𝐴–1-1-onto→𝐵
8		vx	. . . . . . . 8 setvar 𝑥
9	8	cv 1538	. . . . . . 7 class 𝑥
10		vy	. . . . . . . 8 setvar 𝑦
11	10	cv 1538	. . . . . . 7 class 𝑦
12	9, 11, 3	wbr 5070	. . . . . 6 wff 𝑥𝑅𝑦
13	9, 5	cfv 6418	. . . . . . 7 class (𝐻‘𝑥)
14	11, 5	cfv 6418	. . . . . . 7 class (𝐻‘𝑦)
15	13, 14, 4	wbr 5070	. . . . . 6 wff (𝐻‘𝑥)𝑆(𝐻‘𝑦)
16	12, 15	wb 205	. . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
17	16, 10, 1	wral 3063	. . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
18	17, 8, 1	wral 3063	. . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
19	7, 18	wa 395	. 2 wff (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
20	6, 19	wb 205	1 wff (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))

This definition is referenced by:  isoeq1  7168  isoeq2  7169  isoeq3  7170  isoeq4  7171  isoeq5  7172  nfiso  7173  isof1o  7174  isof1oidb  7175  isof1oopb  7176  isorel  7177  soisores  7178  soisoi  7179  isoid  7180  isocnv  7181  isocnv2  7182  isocnv3  7183  isores2  7184  isores3  7186  isotr  7187  isoini2  7190  f1oiso  7202  f1owe  7204  smoiso2  8171  alephiso  9785  compssiso  10061  negiso  11885  om2uzisoi  13602  icopnfhmeo  24012  reefiso  25512  logltb  25660  isoun  30936  mgcf1o  31183  xrmulc1cn  31782  sticksstones3  40032  wepwsolem  40783  alephiso2  41054  iso0  41814  fourierdlem54  43591  rrx2plordisom  45957