Metamath Proof Explorer


Theorem cantnflem2

Description: Lemma for cantnf . (Contributed by Mario Carneiro, 28-May-2015)

Ref Expression
Hypotheses cantnfs.s S=domACNFB
cantnfs.a φAOn
cantnfs.b φBOn
oemapval.t T=xy|zBxzyzwBzwxw=yw
cantnf.c φCA𝑜B
cantnf.s φCranACNFB
cantnf.e φC
Assertion cantnflem2 φAOn2𝑜COn1𝑜

Proof

Step Hyp Ref Expression
1 cantnfs.s S=domACNFB
2 cantnfs.a φAOn
3 cantnfs.b φBOn
4 oemapval.t T=xy|zBxzyzwBzwxw=yw
5 cantnf.c φCA𝑜B
6 cantnf.s φCranACNFB
7 cantnf.e φC
8 oecl AOnBOnA𝑜BOn
9 2 3 8 syl2anc φA𝑜BOn
10 onelon A𝑜BOnCA𝑜BCOn
11 9 5 10 syl2anc φCOn
12 ondif1 COn1𝑜COnC
13 11 7 12 sylanbrc φCOn1𝑜
14 13 eldifbd φ¬C1𝑜
15 ssel A𝑜B1𝑜CA𝑜BC1𝑜
16 5 15 syl5com φA𝑜B1𝑜C1𝑜
17 14 16 mtod φ¬A𝑜B1𝑜
18 oe0m BOn𝑜B=1𝑜B
19 3 18 syl φ𝑜B=1𝑜B
20 difss 1𝑜B1𝑜
21 19 20 eqsstrdi φ𝑜B1𝑜
22 oveq1 A=A𝑜B=𝑜B
23 22 sseq1d A=A𝑜B1𝑜𝑜B1𝑜
24 21 23 syl5ibrcom φA=A𝑜B1𝑜
25 oe1m BOn1𝑜𝑜B=1𝑜
26 eqimss 1𝑜𝑜B=1𝑜1𝑜𝑜B1𝑜
27 3 25 26 3syl φ1𝑜𝑜B1𝑜
28 oveq1 A=1𝑜A𝑜B=1𝑜𝑜B
29 28 sseq1d A=1𝑜A𝑜B1𝑜1𝑜𝑜B1𝑜
30 27 29 syl5ibrcom φA=1𝑜A𝑜B1𝑜
31 24 30 jaod φA=A=1𝑜A𝑜B1𝑜
32 17 31 mtod φ¬A=A=1𝑜
33 elpri A1𝑜A=A=1𝑜
34 df2o3 2𝑜=1𝑜
35 33 34 eleq2s A2𝑜A=A=1𝑜
36 32 35 nsyl φ¬A2𝑜
37 2 36 eldifd φAOn2𝑜
38 37 13 jca φAOn2𝑜COn1𝑜