Metamath Proof Explorer


Theorem om2uzf1oi

Description: G (see om2uz0i ) is a one-to-one onto mapping. (Contributed by NM, 3-Oct-2004) (Revised by Mario Carneiro, 13-Sep-2013)

Ref Expression
Hypotheses om2uz.1 C
om2uz.2 G = rec x V x + 1 C ω
Assertion om2uzf1oi G : ω 1-1 onto C

Proof

Step Hyp Ref Expression
1 om2uz.1 C
2 om2uz.2 G = rec x V x + 1 C ω
3 frfnom rec x V x + 1 C ω Fn ω
4 2 fneq1i G Fn ω rec x V x + 1 C ω Fn ω
5 3 4 mpbir G Fn ω
6 1 2 om2uzrani ran G = C
7 6 eqimssi ran G C
8 df-f G : ω C G Fn ω ran G C
9 5 7 8 mpbir2an G : ω C
10 1 2 om2uzuzi y ω G y C
11 eluzelz G y C G y
12 10 11 syl y ω G y
13 12 zred y ω G y
14 1 2 om2uzuzi z ω G z C
15 eluzelz G z C G z
16 14 15 syl z ω G z
17 16 zred z ω G z
18 lttri3 G y G z G y = G z ¬ G y < G z ¬ G z < G y
19 13 17 18 syl2an y ω z ω G y = G z ¬ G y < G z ¬ G z < G y
20 ioran ¬ G y < G z G z < G y ¬ G y < G z ¬ G z < G y
21 19 20 bitr4di y ω z ω G y = G z ¬ G y < G z G z < G y
22 nnord y ω Ord y
23 nnord z ω Ord z
24 ordtri3 Ord y Ord z y = z ¬ y z z y
25 22 23 24 syl2an y ω z ω y = z ¬ y z z y
26 25 con2bid y ω z ω y z z y ¬ y = z
27 1 2 om2uzlti y ω z ω y z G y < G z
28 1 2 om2uzlti z ω y ω z y G z < G y
29 28 ancoms y ω z ω z y G z < G y
30 27 29 orim12d y ω z ω y z z y G y < G z G z < G y
31 26 30 sylbird y ω z ω ¬ y = z G y < G z G z < G y
32 31 con1d y ω z ω ¬ G y < G z G z < G y y = z
33 21 32 sylbid y ω z ω G y = G z y = z
34 33 rgen2 y ω z ω G y = G z y = z
35 dff13 G : ω 1-1 C G : ω C y ω z ω G y = G z y = z
36 9 34 35 mpbir2an G : ω 1-1 C
37 dff1o5 G : ω 1-1 onto C G : ω 1-1 C ran G = C
38 36 6 37 mpbir2an G : ω 1-1 onto C