Definition df-isom 6485

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 6477	. 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
7	1, 2, 5	wf1o 6475	. . 3 wff 𝐻:𝐴–1-1-onto→𝐵
8		vx	. . . . . . . 8 setvar 𝑥
9	8	cv 1540	. . . . . . 7 class 𝑥
10		vy	. . . . . . . 8 setvar 𝑦
11	10	cv 1540	. . . . . . 7 class 𝑦
12	9, 11, 3	wbr 5086	. . . . . 6 wff 𝑥𝑅𝑦
13	9, 5	cfv 6476	. . . . . . 7 class (𝐻‘𝑥)
14	11, 5	cfv 6476	. . . . . . 7 class (𝐻‘𝑦)
15	13, 14, 4	wbr 5086	. . . . . 6 wff (𝐻‘𝑥)𝑆(𝐻‘𝑦)
16	12, 15	wb 206	. . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
17	16, 10, 1	wral 3047	. . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
18	17, 8, 1	wral 3047	. . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
19	7, 18	wa 395	. 2 wff (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
20	6, 19	wb 206	1 wff (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))

This definition is referenced by:  isoeq1  7246  isoeq2  7247  isoeq3  7248  isoeq4  7249  isoeq5  7250  nfiso  7251  isof1o  7252  isof1oidb  7253  isof1oopb  7254  isorel  7255  soisores  7256  soisoi  7257  isoid  7258  isocnv  7259  isocnv2  7260  isocnv3  7261  isores2  7262  isores3  7264  isotr  7265  isoini2  7268  f1oiso  7280  f1owe  7282  smoiso2  8284  alephiso  9984  compssiso  10260  negiso  12097  om2uzisoi  13856  icopnfhmeo  24863  reefiso  26380  logltb  26531  onsiso  28200  om2noseqiso  28227  isoun  32675  mgcf1o  32976  xrmulc1cn  33935  sticksstones3  42181  wepwsolem  43075  alephiso2  43591  iso0  44340  fourierdlem54  46198  rrx2plordisom  48755