Metamath Proof Explorer

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 ⊢ H Isom R , S A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cH class H
1 cR class R
2 cS class S
3 cA class A
4 cB class B
5 3 4 1 2 0 wiso wff H Isom R , S A B
6 3 4 0 wf1o wff H : A ⟶ 1-1 onto B
7 vx setvar x
8 vy setvar y
9 7 cv setvar x
10 8 cv setvar y
11 9 10 1 wbr wff x R y
12 9 0 cfv class H ⁡ x
13 10 0 cfv class H ⁡ y
14 12 13 2 wbr wff H ⁡ x S H ⁡ y
15 11 14 wb wff x R y ↔ H ⁡ x S H ⁡ y
16 15 8 3 wral wff ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y
17 16 7 3 wral wff ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y
18 6 17 wa wff H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y
19 5 18 wb wff H Isom R , S A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y