Definition df-isom 6545

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 6537	. 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
7	1, 2, 5	wf1o 6535	. . 3 wff 𝐻:𝐴–1-1-onto→𝐵
8		vx	. . . . . . . 8 setvar 𝑥
9	8	cv 1568	. . . . . . 7 class 𝑥
10		vy	. . . . . . . 8 setvar 𝑦
11	10	cv 1568	. . . . . . 7 class 𝑦
12	9, 11, 3	wbr 5108	. . . . . 6 wff 𝑥𝑅𝑦
13	9, 5	cfv 6536	. . . . . . 7 class (𝐻‘𝑥)
14	11, 5	cfv 6536	. . . . . . 7 class (𝐻‘𝑦)
15	13, 14, 4	wbr 5108	. . . . . 6 wff (𝐻‘𝑥)𝑆(𝐻‘𝑦)
16	12, 15	wb 209	. . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
17	16, 10, 1	wral 3078	. . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
18	17, 8, 1	wral 3078	. . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))
19	7, 18	wa 400	. 2 wff (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
20	6, 19	wb 209	1 wff (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))

This definition is used by:  isoeq1  7315  isoeq2  7316  isoeq3  7317  isoeq4  7318  isoeq5  7319  nfiso  7320  isof1o  7321  isof1oidb  7322  isof1oopb  7323  isorel  7324  soisores  7325  soisoi  7326  isoid  7327  isocnv  7328  isocnv2  7329  isocnv3  7330  isores2  7331  isores3  7333  isotr  7334  isoini2  7337  f1oiso  7349  f1owe  7351  f1oweOLD  7352  smoiso2  8354  alephiso  10089  compssiso  10364  negiso  12201  om2uzisoi  13997  icopnfhmeo  25113  reefiso  26622  logltb  26776  oniso  28475  om2noseqiso  28506  isoun  33058  mgcf1o  33332  xrmulc1cn  34329  vonf1osev  35604  sticksstones3  42943  wepwsolem  43797  alephiso2  44312  iso0  45045  hashomiso  45762  fourierdlem54  46902  rrx2plordisom  49531