This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cantnflem2

Description: Lemma for cantnf . (Contributed by Mario Carneiro, 28-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 )
Assertion cantnflem2 
|- ( ph -> ( A e. ( On \ 2o ) /\ C e. ( On \ 1o ) ) )

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 oecl 
 |-  ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
9 2 3 8 syl2anc 
 |-  ( ph -> ( A ^o B ) e. On )
10 onelon 
 |-  ( ( ( A ^o B ) e. On /\ C e. ( A ^o B ) ) -> C e. On )
11 9 5 10 syl2anc 
 |-  ( ph -> C e. On )
12 ondif1 
 |-  ( C e. ( On \ 1o ) <-> ( C e. On /\ (/) e. C ) )
13 11 7 12 sylanbrc 
 |-  ( ph -> C e. ( On \ 1o ) )
14 13 eldifbd 
 |-  ( ph -> -. C e. 1o )
15 ssel 
 |-  ( ( A ^o B ) C_ 1o -> ( C e. ( A ^o B ) -> C e. 1o ) )
16 5 15 syl5com 
 |-  ( ph -> ( ( A ^o B ) C_ 1o -> C e. 1o ) )
17 14 16 mtod 
 |-  ( ph -> -. ( A ^o B ) C_ 1o )
18 oe0m 
 |-  ( B e. On -> ( (/) ^o B ) = ( 1o \ B ) )
19 3 18 syl 
 |-  ( ph -> ( (/) ^o B ) = ( 1o \ B ) )
20 difss 
 |-  ( 1o \ B ) C_ 1o
21 19 20 eqsstrdi 
 |-  ( ph -> ( (/) ^o B ) C_ 1o )
22 oveq1 
 |-  ( A = (/) -> ( A ^o B ) = ( (/) ^o B ) )
23 22 sseq1d 
 |-  ( A = (/) -> ( ( A ^o B ) C_ 1o <-> ( (/) ^o B ) C_ 1o ) )
24 21 23 syl5ibrcom 
 |-  ( ph -> ( A = (/) -> ( A ^o B ) C_ 1o ) )
25 oe1m 
 |-  ( B e. On -> ( 1o ^o B ) = 1o )
26 eqimss 
 |-  ( ( 1o ^o B ) = 1o -> ( 1o ^o B ) C_ 1o )
27 3 25 26 3syl 
 |-  ( ph -> ( 1o ^o B ) C_ 1o )
28 oveq1 
 |-  ( A = 1o -> ( A ^o B ) = ( 1o ^o B ) )
29 28 sseq1d 
 |-  ( A = 1o -> ( ( A ^o B ) C_ 1o <-> ( 1o ^o B ) C_ 1o ) )
30 27 29 syl5ibrcom 
 |-  ( ph -> ( A = 1o -> ( A ^o B ) C_ 1o ) )
31 24 30 jaod 
 |-  ( ph -> ( ( A = (/) \/ A = 1o ) -> ( A ^o B ) C_ 1o ) )
32 17 31 mtod 
 |-  ( ph -> -. ( A = (/) \/ A = 1o ) )
33 elpri 
 |-  ( A e. { (/) , 1o } -> ( A = (/) \/ A = 1o ) )
34 df2o3 
 |-  2o = { (/) , 1o }
35 33 34 eleq2s 
 |-  ( A e. 2o -> ( A = (/) \/ A = 1o ) )
36 32 35 nsyl 
 |-  ( ph -> -. A e. 2o )
37 2 36 eldifd 
 |-  ( ph -> A e. ( On \ 2o ) )
38 37 13 jca 
 |-  ( ph -> ( A e. ( On \ 2o ) /\ C e. ( On \ 1o ) ) )