Definition df-isom 5813

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 5805	. 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
7	1, 2, 5	wf1o 5803	. . 3 wff 𝐻:𝐴–1-1-onto→𝐵
8		vx	. . . . . . . 8 setvar 𝑥
9	8	cv 1474	. . . . . . 7 class 𝑥
10		vy	. . . . . . . 8 setvar 𝑦
11	10	cv 1474	. . . . . . 7 class 𝑦
12	9, 11, 3	wbr 4583	. . . . . 6 wff 𝑥𝑅𝑦
13	9, 5	cfv 5804	. . . . . . 7 class (𝐻‘𝑥)
14	11, 5	cfv 5804	. . . . . . 7 class (𝐻‘𝑦)
15	13, 14, 4	wbr 4583	. . . . . 6 wff (𝐻‘𝑥)𝑆(𝐻‘𝑦)
16	12, 15	wb 195	. . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
17	16, 10, 1	wral 2896	. . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
18	17, 8, 1	wral 2896	. . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
19	7, 18	wa 383	. 2 wff (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
20	6, 19	wb 195	1 wff (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))

This definition is referenced by:  isoeq1  6467  isoeq2  6468  isoeq3  6469  isoeq4  6470  isoeq5  6471  nfiso  6472  isof1o  6473  isof1oidb  6474  isof1oopb  6475  isorel  6476  soisores  6477  soisoi  6478  isoid  6479  isocnv  6480  isocnv2  6481  isocnv3  6482  isores2  6483  isores3  6485  isotr  6486  isoini2  6489  f1oiso  6501  f1owe  6503  smoiso2  7353  alephiso  8804  compssiso  9079  negiso  10880  om2uzisoi  12615  icopnfhmeo  22550  reefiso  24006  logltb  24150  isoun  28862  xrmulc1cn  29304  wepwsolem  36630  iso0  37528  fourierdlem54  39053