Metamath Proof Explorer

Theorem cantnflem4

Description: Lemma for cantnf . Complete the induction step of cantnflem3 . (Contributed by Mario Carneiro, 25-May-2015)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
oemapval.t 
|- T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
cantnf.c 
|- ( ph -> C e. ( A ^o B ) )
cantnf.s 
|- ( ph -> C C_ ran ( A CNF B ) )
cantnf.e 
|- ( ph -> (/) e. C )
cantnf.x 
|- X = U. |^| { c e. On | C e. ( A ^o c ) }
cantnf.p 
|- P = ( iota d E. a e. On E. b e. ( A ^o X ) ( d = <. a , b >. /\ ( ( ( A ^o X ) .o a ) +o b ) = C ) )
cantnf.y 
|- Y = ( 1st ` P )
cantnf.z 
|- Z = ( 2nd ` P )
Assertion cantnflem4 
|- ( ph -> C e. ran ( A CNF B ) )

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 oemapval.t 
 |-  T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
5 cantnf.c 
 |-  ( ph -> C e. ( A ^o B ) )
6 cantnf.s 
 |-  ( ph -> C C_ ran ( A CNF B ) )
7 cantnf.e 
 |-  ( ph -> (/) e. C )
8 cantnf.x 
 |-  X = U. |^| { c e. On | C e. ( A ^o c ) }
9 cantnf.p 
 |-  P = ( iota d E. a e. On E. b e. ( A ^o X ) ( d = <. a , b >. /\ ( ( ( A ^o X ) .o a ) +o b ) = C ) )
10 cantnf.y 
 |-  Y = ( 1st ` P )
11 cantnf.z 
 |-  Z = ( 2nd ` P )
12 1 2 3 4 5 6 7 cantnflem2 
 |-  ( ph -> ( A e. ( On \ 2o ) /\ C e. ( On \ 1o ) ) )
13 eqid 
 |-  X = X
14 eqid 
 |-  Y = Y
15 eqid 
 |-  Z = Z
16 13 14 15 3pm3.2i 
 |-  ( X = X /\ Y = Y /\ Z = Z )
17 8 9 10 11 oeeui 
 |-  ( ( A e. ( On \ 2o ) /\ C e. ( On \ 1o ) ) -> ( ( ( X e. On /\ Y e. ( A \ 1o ) /\ Z e. ( A ^o X ) ) /\ ( ( ( A ^o X ) .o Y ) +o Z ) = C ) <-> ( X = X /\ Y = Y /\ Z = Z ) ) )
18 16 17 mpbiri 
 |-  ( ( A e. ( On \ 2o ) /\ C e. ( On \ 1o ) ) -> ( ( X e. On /\ Y e. ( A \ 1o ) /\ Z e. ( A ^o X ) ) /\ ( ( ( A ^o X ) .o Y ) +o Z ) = C ) )
19 12 18 syl 
 |-  ( ph -> ( ( X e. On /\ Y e. ( A \ 1o ) /\ Z e. ( A ^o X ) ) /\ ( ( ( A ^o X ) .o Y ) +o Z ) = C ) )
20 19 simpld 
 |-  ( ph -> ( X e. On /\ Y e. ( A \ 1o ) /\ Z e. ( A ^o X ) ) )
21 20 simp1d 
 |-  ( ph -> X e. On )
22 oecl 
 |-  ( ( A e. On /\ X e. On ) -> ( A ^o X ) e. On )
23 2 21 22 syl2anc 
 |-  ( ph -> ( A ^o X ) e. On )
24 20 simp2d 
 |-  ( ph -> Y e. ( A \ 1o ) )
25 24 eldifad 
 |-  ( ph -> Y e. A )
26 onelon 
 |-  ( ( A e. On /\ Y e. A ) -> Y e. On )
27 2 25 26 syl2anc 
 |-  ( ph -> Y e. On )
28 omcl 
 |-  ( ( ( A ^o X ) e. On /\ Y e. On ) -> ( ( A ^o X ) .o Y ) e. On )
29 23 27 28 syl2anc 
 |-  ( ph -> ( ( A ^o X ) .o Y ) e. On )
30 20 simp3d 
 |-  ( ph -> Z e. ( A ^o X ) )
31 onelon 
 |-  ( ( ( A ^o X ) e. On /\ Z e. ( A ^o X ) ) -> Z e. On )
32 23 30 31 syl2anc 
 |-  ( ph -> Z e. On )
33 oaword1 
 |-  ( ( ( ( A ^o X ) .o Y ) e. On /\ Z e. On ) -> ( ( A ^o X ) .o Y ) C_ ( ( ( A ^o X ) .o Y ) +o Z ) )
34 29 32 33 syl2anc 
 |-  ( ph -> ( ( A ^o X ) .o Y ) C_ ( ( ( A ^o X ) .o Y ) +o Z ) )
35 dif1o 
 |-  ( Y e. ( A \ 1o ) <-> ( Y e. A /\ Y =/= (/) ) )
36 35 simprbi 
 |-  ( Y e. ( A \ 1o ) -> Y =/= (/) )
37 24 36 syl 
 |-  ( ph -> Y =/= (/) )
38 on0eln0 
 |-  ( Y e. On -> ( (/) e. Y <-> Y =/= (/) ) )
39 27 38 syl 
 |-  ( ph -> ( (/) e. Y <-> Y =/= (/) ) )
40 37 39 mpbird 
 |-  ( ph -> (/) e. Y )
41 omword1 
 |-  ( ( ( ( A ^o X ) e. On /\ Y e. On ) /\ (/) e. Y ) -> ( A ^o X ) C_ ( ( A ^o X ) .o Y ) )
42 23 27 40 41 syl21anc 
 |-  ( ph -> ( A ^o X ) C_ ( ( A ^o X ) .o Y ) )
43 42 30 sseldd 
 |-  ( ph -> Z e. ( ( A ^o X ) .o Y ) )
44 34 43 sseldd 
 |-  ( ph -> Z e. ( ( ( A ^o X ) .o Y ) +o Z ) )
45 19 simprd 
 |-  ( ph -> ( ( ( A ^o X ) .o Y ) +o Z ) = C )
46 44 45 eleqtrd 
 |-  ( ph -> Z e. C )
47 6 46 sseldd 
 |-  ( ph -> Z e. ran ( A CNF B ) )
48 1 2 3 cantnff 
 |-  ( ph -> ( A CNF B ) : S --> ( A ^o B ) )
49 ffn 
 |-  ( ( A CNF B ) : S --> ( A ^o B ) -> ( A CNF B ) Fn S )
50 fvelrnb 
 |-  ( ( A CNF B ) Fn S -> ( Z e. ran ( A CNF B ) <-> E. g e. S ( ( A CNF B ) ` g ) = Z ) )
51 48 49 50 3syl 
 |-  ( ph -> ( Z e. ran ( A CNF B ) <-> E. g e. S ( ( A CNF B ) ` g ) = Z ) )
52 47 51 mpbid 
 |-  ( ph -> E. g e. S ( ( A CNF B ) ` g ) = Z )
53 2 adantr 
 |-  ( ( ph /\ ( g e. S /\ ( ( A CNF B ) ` g ) = Z ) ) -> A e. On )
54 3 adantr 
 |-  ( ( ph /\ ( g e. S /\ ( ( A CNF B ) ` g ) = Z ) ) -> B e. On )
55 5 adantr 
 |-  ( ( ph /\ ( g e. S /\ ( ( A CNF B ) ` g ) = Z ) ) -> C e. ( A ^o B ) )
56 6 adantr 
 |-  ( ( ph /\ ( g e. S /\ ( ( A CNF B ) ` g ) = Z ) ) -> C C_ ran ( A CNF B ) )
57 7 adantr 
 |-  ( ( ph /\ ( g e. S /\ ( ( A CNF B ) ` g ) = Z ) ) -> (/) e. C )
58 simprl 
 |-  ( ( ph /\ ( g e. S /\ ( ( A CNF B ) ` g ) = Z ) ) -> g e. S )
59 simprr 
 |-  ( ( ph /\ ( g e. S /\ ( ( A CNF B ) ` g ) = Z ) ) -> ( ( A CNF B ) ` g ) = Z )
60 eqid 
 |-  ( t e. B |-> if ( t = X , Y , ( g ` t ) ) ) = ( t e. B |-> if ( t = X , Y , ( g ` t ) ) )
61 1 53 54 4 55 56 57 8 9 10 11 58 59 60 cantnflem3 
 |-  ( ( ph /\ ( g e. S /\ ( ( A CNF B ) ` g ) = Z ) ) -> C e. ran ( A CNF B ) )
62 52 61 rexlimddv 
 |-  ( ph -> C e. ran ( A CNF B ) )