Definition df-isom 6582

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 6574	. 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
7	1, 2, 5	wf1o 6572	. . 3 wff 𝐻:𝐴–1-1-onto→𝐵
8		vx	. . . . . . . 8 setvar 𝑥
9	8	cv 1536	. . . . . . 7 class 𝑥
10		vy	. . . . . . . 8 setvar 𝑦
11	10	cv 1536	. . . . . . 7 class 𝑦
12	9, 11, 3	wbr 5166	. . . . . 6 wff 𝑥𝑅𝑦
13	9, 5	cfv 6573	. . . . . . 7 class (𝐻‘𝑥)
14	11, 5	cfv 6573	. . . . . . 7 class (𝐻‘𝑦)
15	13, 14, 4	wbr 5166	. . . . . 6 wff (𝐻‘𝑥)𝑆(𝐻‘𝑦)
16	12, 15	wb 206	. . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
17	16, 10, 1	wral 3067	. . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
18	17, 8, 1	wral 3067	. . 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  7353  isoeq2  7354  isoeq3  7355  isoeq4  7356  isoeq5  7357  nfiso  7358  isof1o  7359  isof1oidb  7360  isof1oopb  7361  isorel  7362  soisores  7363  soisoi  7364  isoid  7365  isocnv  7366  isocnv2  7367  isocnv3  7368  isores2  7369  isores3  7371  isotr  7372  isoini2  7375  f1oiso  7387  f1owe  7389  smoiso2  8425  alephiso  10167  compssiso  10443  negiso  12275  om2uzisoi  14005  icopnfhmeo  24993  reefiso  26510  logltb  26660  om2noseqiso  28326  isoun  32713  mgcf1o  32976  xrmulc1cn  33876  sticksstones3  42105  wepwsolem  42999  alephiso2  43520  iso0  44276  fourierdlem54  46081  rrx2plordisom  48457