Metamath Proof Explorer


Theorem nosepnelem

Description: Lemma for nosepne . (Contributed by Scott Fenton, 24-Nov-2021)

Ref Expression
Assertion nosepnelem ANoBNoA<sBAxOn|AxBxBxOn|AxBx

Proof

Step Hyp Ref Expression
1 sltval2 ANoBNoA<sBAxOn|AxBx1𝑜1𝑜2𝑜2𝑜BxOn|AxBx
2 fvex AxOn|AxBxV
3 fvex BxOn|AxBxV
4 2 3 brtp AxOn|AxBx1𝑜1𝑜2𝑜2𝑜BxOn|AxBxAxOn|AxBx=1𝑜BxOn|AxBx=AxOn|AxBx=1𝑜BxOn|AxBx=2𝑜AxOn|AxBx=BxOn|AxBx=2𝑜
5 1n0 1𝑜
6 simpl AxOn|AxBx=1𝑜BxOn|AxBx=AxOn|AxBx=1𝑜
7 simpr AxOn|AxBx=1𝑜BxOn|AxBx=BxOn|AxBx=
8 6 7 neeq12d AxOn|AxBx=1𝑜BxOn|AxBx=AxOn|AxBxBxOn|AxBx1𝑜
9 5 8 mpbiri AxOn|AxBx=1𝑜BxOn|AxBx=AxOn|AxBxBxOn|AxBx
10 df-2o 2𝑜=suc1𝑜
11 df-1o 1𝑜=suc
12 10 11 eqeq12i 2𝑜=1𝑜suc1𝑜=suc
13 1on 1𝑜On
14 0elon On
15 suc11 1𝑜OnOnsuc1𝑜=suc1𝑜=
16 13 14 15 mp2an suc1𝑜=suc1𝑜=
17 12 16 bitri 2𝑜=1𝑜1𝑜=
18 17 necon3bii 2𝑜1𝑜1𝑜
19 5 18 mpbir 2𝑜1𝑜
20 19 necomi 1𝑜2𝑜
21 simpl AxOn|AxBx=1𝑜BxOn|AxBx=2𝑜AxOn|AxBx=1𝑜
22 simpr AxOn|AxBx=1𝑜BxOn|AxBx=2𝑜BxOn|AxBx=2𝑜
23 21 22 neeq12d AxOn|AxBx=1𝑜BxOn|AxBx=2𝑜AxOn|AxBxBxOn|AxBx1𝑜2𝑜
24 20 23 mpbiri AxOn|AxBx=1𝑜BxOn|AxBx=2𝑜AxOn|AxBxBxOn|AxBx
25 2on 2𝑜On
26 25 elexi 2𝑜V
27 26 prid2 2𝑜1𝑜2𝑜
28 27 nosgnn0i 2𝑜
29 simpl AxOn|AxBx=BxOn|AxBx=2𝑜AxOn|AxBx=
30 simpr AxOn|AxBx=BxOn|AxBx=2𝑜BxOn|AxBx=2𝑜
31 29 30 neeq12d AxOn|AxBx=BxOn|AxBx=2𝑜AxOn|AxBxBxOn|AxBx2𝑜
32 28 31 mpbiri AxOn|AxBx=BxOn|AxBx=2𝑜AxOn|AxBxBxOn|AxBx
33 9 24 32 3jaoi AxOn|AxBx=1𝑜BxOn|AxBx=AxOn|AxBx=1𝑜BxOn|AxBx=2𝑜AxOn|AxBx=BxOn|AxBx=2𝑜AxOn|AxBxBxOn|AxBx
34 4 33 sylbi AxOn|AxBx1𝑜1𝑜2𝑜2𝑜BxOn|AxBxAxOn|AxBxBxOn|AxBx
35 1 34 syl6bi ANoBNoA<sBAxOn|AxBxBxOn|AxBx
36 35 3impia ANoBNoA<sBAxOn|AxBxBxOn|AxBx