This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Power Sets Functions 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 → 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )