Definition df-isom

Description: Define the isomorphism predicate. We read this as " H is an R , S isomorphism of A onto B ". Normally, R and S are ordering relations on A and B respectively. Definition 6.28 of TakeutiZaring p. 32, whose notation is the same as ours except that R and S are subscripts. (Contributed by NM, 4-Mar-1997)

	Ref	Expression
Assertion	df-isom	⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cH	⊢ 𝐻
1		cR	⊢ 𝑅
2		cS	⊢ 𝑆
3		cA	⊢ 𝐴
4		cB	⊢ 𝐵
5	3 4 1 2 0	wiso	⊢ 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 )
6	3 4 0	wf1o	⊢ 𝐻 : 𝐴 –1-1-onto→ 𝐵
7		vx	⊢ 𝑥
8		vy	⊢ 𝑦
9	7	cv	⊢ 𝑥
10	8	cv	⊢ 𝑦
11	9 10 1	wbr	⊢ 𝑥 𝑅 𝑦
12	9 0	cfv	⊢ ( 𝐻 ‘ 𝑥 )
13	10 0	cfv	⊢ ( 𝐻 ‘ 𝑦 )
14	12 13 2	wbr	⊢ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 )
15	11 14	wb	⊢ ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) )
16	15 8 3	wral	⊢ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) )
17	16 7 3	wral	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) )
18	6 17	wa	⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
19	5 18	wb	⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )