Definition df-isom 6564

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

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 6556	. 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
7	1, 2, 5	wf1o 6554	. . 3 wff 𝐻:𝐴⟶1-1onto𝐵
8		vx	. . . . . . . 8 setvar 𝑥
9	8	cv 1569	. . . . . . 7 class 𝑥
10		vy	. . . . . . . 8 setvar 𝑦
11	10	cv 1569	. . . . . . 7 class 𝑦
12	9, 11, 3	wbr 5106	. . . . . 6 wff 𝑥𝑅𝑦
13	9, 5	cfv 6555	. . . . . . 7 class (𝐻‘𝑥)
14	11, 5	cfv 6555	. . . . . . 7 class (𝐻‘𝑦)
15	13, 14, 4	wbr 5106	. . . . . 6 wff (𝐻‘𝑥)𝑆(𝐻‘𝑦)
16	12, 15	wb 209	. . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
17	16, 10, 1	wral 3080	. . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
18	17, 8, 1	wral 3080	. . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
19	7, 18	wa 401	. 2 wff (𝐻:𝐴⟶1-1onto𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
20	6, 19	wb 209	1 wff (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴⟶1-1onto𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))

This definition is used by:  isoeq1  7345  isoeq2  7346  isoeq3  7347  isoeq4  7348  isoeq5  7349  nfiso  7350  isof1o  7351  isof1oidb  7352  isof1oopb  7353  isorel  7354  soisores  7355  soisoi  7356  isoid  7357  isocnv  7358  isocnv2  7359  isocnv3  7360  isores2  7361  isores3  7363  isotr  7364  isoini2  7367  f1oiso  7379  f1owe  7381  f1oweOLD  7382  smoiso2  8402  alephiso  10201  compssiso  10476  negiso  12321  om2uzisoi  14121  icopnfhmeo  25291  reefiso  26802  logltb  26955  oniso  28684  om2noseqiso  28715  isoun  33363  mgcf1o  33631  xrmulc1cn  34629  vonf1osev  36039  sticksstones3  43389  wepwsolem  44240  alephiso2  44749  iso0  45481  hashomiso  46208  fourierdlem54  47373  rrx2plordisom  50039