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 ) ) )