Metamath Proof Explorer

Theorem cantnfp1lem2

Description: Lemma for cantnfp1 . (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 30-Jun-2019)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
cantnfp1.g 
|- ( ph -> G e. S )
cantnfp1.x 
|- ( ph -> X e. B )
cantnfp1.y 
|- ( ph -> Y e. A )
cantnfp1.s 
|- ( ph -> ( G supp (/) ) C_ X )
cantnfp1.f 
|- F = ( t e. B |-> if ( t = X , Y , ( G ` t ) ) )
cantnfp1.e 
|- ( ph -> (/) e. Y )
cantnfp1.o 
|- O = OrdIso ( _E , ( F supp (/) ) )
Assertion cantnfp1lem2 
|- ( ph -> dom O = suc U. dom O )

Proof

Step Hyp Ref Expression
1 cantnfs.s 
 |-  S = dom ( A CNF B )
2 cantnfs.a 
 |-  ( ph -> A e. On )
3 cantnfs.b 
 |-  ( ph -> B e. On )
4 cantnfp1.g 
 |-  ( ph -> G e. S )
5 cantnfp1.x 
 |-  ( ph -> X e. B )
6 cantnfp1.y 
 |-  ( ph -> Y e. A )
7 cantnfp1.s 
 |-  ( ph -> ( G supp (/) ) C_ X )
8 cantnfp1.f 
 |-  F = ( t e. B |-> if ( t = X , Y , ( G ` t ) ) )
9 cantnfp1.e 
 |-  ( ph -> (/) e. Y )
10 cantnfp1.o 
 |-  O = OrdIso ( _E , ( F supp (/) ) )
11 iftrue 
 |-  ( t = X -> if ( t = X , Y , ( G ` t ) ) = Y )
12 8 11 5 6 fvmptd3 
 |-  ( ph -> ( F ` X ) = Y )
13 9 ne0d 
 |-  ( ph -> Y =/= (/) )
14 12 13 eqnetrd 
 |-  ( ph -> ( F ` X ) =/= (/) )
15 6 adantr 
 |-  ( ( ph /\ t e. B ) -> Y e. A )
16 1 2 3 cantnfs 
 |-  ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) )
17 4 16 mpbid 
 |-  ( ph -> ( G : B --> A /\ G finSupp (/) ) )
18 17 simpld 
 |-  ( ph -> G : B --> A )
19 18 ffvelcdmda 
 |-  ( ( ph /\ t e. B ) -> ( G ` t ) e. A )
20 15 19 ifcld 
 |-  ( ( ph /\ t e. B ) -> if ( t = X , Y , ( G ` t ) ) e. A )
21 20 8 fmptd 
 |-  ( ph -> F : B --> A )
22 21 ffnd 
 |-  ( ph -> F Fn B )
23 9 elexd 
 |-  ( ph -> (/) e. _V )
24 elsuppfn 
 |-  ( ( F Fn B /\ B e. On /\ (/) e. _V ) -> ( X e. ( F supp (/) ) <-> ( X e. B /\ ( F ` X ) =/= (/) ) ) )
25 22 3 23 24 syl3anc 
 |-  ( ph -> ( X e. ( F supp (/) ) <-> ( X e. B /\ ( F ` X ) =/= (/) ) ) )
26 5 14 25 mpbir2and 
 |-  ( ph -> X e. ( F supp (/) ) )
27 n0i 
 |-  ( X e. ( F supp (/) ) -> -. ( F supp (/) ) = (/) )
28 26 27 syl 
 |-  ( ph -> -. ( F supp (/) ) = (/) )
29 ovexd 
 |-  ( ph -> ( F supp (/) ) e. _V )
30 1 2 3 4 5 6 7 8 cantnfp1lem1 
 |-  ( ph -> F e. S )
31 1 2 3 10 30 cantnfcl 
 |-  ( ph -> ( _E We ( F supp (/) ) /\ dom O e. _om ) )
32 31 simpld 
 |-  ( ph -> _E We ( F supp (/) ) )
33 10 oien 
 |-  ( ( ( F supp (/) ) e. _V /\ _E We ( F supp (/) ) ) -> dom O ~~ ( F supp (/) ) )
34 29 32 33 syl2anc 
 |-  ( ph -> dom O ~~ ( F supp (/) ) )
35 breq1 
 |-  ( dom O = (/) -> ( dom O ~~ ( F supp (/) ) <-> (/) ~~ ( F supp (/) ) ) )
36 ensymb 
 |-  ( (/) ~~ ( F supp (/) ) <-> ( F supp (/) ) ~~ (/) )
37 en0 
 |-  ( ( F supp (/) ) ~~ (/) <-> ( F supp (/) ) = (/) )
38 36 37 bitri 
 |-  ( (/) ~~ ( F supp (/) ) <-> ( F supp (/) ) = (/) )
39 35 38 bitrdi 
 |-  ( dom O = (/) -> ( dom O ~~ ( F supp (/) ) <-> ( F supp (/) ) = (/) ) )
40 34 39 syl5ibcom 
 |-  ( ph -> ( dom O = (/) -> ( F supp (/) ) = (/) ) )
41 28 40 mtod 
 |-  ( ph -> -. dom O = (/) )
42 31 simprd 
 |-  ( ph -> dom O e. _om )
43 nnlim 
 |-  ( dom O e. _om -> -. Lim dom O )
44 42 43 syl 
 |-  ( ph -> -. Lim dom O )
45 ioran 
 |-  ( -. ( dom O = (/) \/ Lim dom O ) <-> ( -. dom O = (/) /\ -. Lim dom O ) )
46 41 44 45 sylanbrc 
 |-  ( ph -> -. ( dom O = (/) \/ Lim dom O ) )
47 nnord 
 |-  ( dom O e. _om -> Ord dom O )
48 unizlim 
 |-  ( Ord dom O -> ( dom O = U. dom O <-> ( dom O = (/) \/ Lim dom O ) ) )
49 42 47 48 3syl 
 |-  ( ph -> ( dom O = U. dom O <-> ( dom O = (/) \/ Lim dom O ) ) )
50 46 49 mtbird 
 |-  ( ph -> -. dom O = U. dom O )
51 orduniorsuc 
 |-  ( Ord dom O -> ( dom O = U. dom O \/ dom O = suc U. dom O ) )
52 42 47 51 3syl 
 |-  ( ph -> ( dom O = U. dom O \/ dom O = suc U. dom O ) )
53 52 ord 
 |-  ( ph -> ( -. dom O = U. dom O -> dom O = suc U. dom O ) )
54 50 53 mpd 
 |-  ( ph -> dom O = suc U. dom O )