Metamath Proof Explorer

Theorem nadddilem1

Description: Lemma for nadddi . Prove a subcase of the reverse implication. (Contributed by Scott Fenton, 31-Jul-2026)

Ref Expression
Hypotheses nadddilem1.1 
|- ( ph -> A e. On )
nadddilem1.2 
|- ( ph -> B e. On )
nadddilem1.3 
|- ( ph -> C e. On )
nadddilem1.4 
|- ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) )
nadddilem1.5 
|- ( ph -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) )
nadddilem1.6 
|- ( ph -> A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) )
Assertion nadddilem1 
|- ( ( ph /\ Y e. ( A .no C ) ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) )

Proof

Step Hyp Ref Expression
1 nadddilem1.1 
 |-  ( ph -> A e. On )
2 nadddilem1.2 
 |-  ( ph -> B e. On )
3 nadddilem1.3 
 |-  ( ph -> C e. On )
4 nadddilem1.4 
 |-  ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) )
5 nadddilem1.5 
 |-  ( ph -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) )
6 nadddilem1.6 
 |-  ( ph -> A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) )
7 1 adantr 
 |-  ( ( ph /\ Y e. ( A .no C ) ) -> A e. On )
8 3 adantr 
 |-  ( ( ph /\ Y e. ( A .no C ) ) -> C e. On )
9 7 8 nmulcld 
 |-  ( ( ph /\ Y e. ( A .no C ) ) -> ( A .no C ) e. On )
10 simpr 
 |-  ( ( ph /\ Y e. ( A .no C ) ) -> Y e. ( A .no C ) )
11 9 10 onelond 
 |-  ( ( ph /\ Y e. ( A .no C ) ) -> Y e. On )
12 ltnmul 
 |-  ( ( Y e. On /\ A e. On /\ C e. On ) -> ( Y e. ( A .no C ) <-> E. z e. A E. w e. C ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) )
13 11 7 8 12 syl3anc 
 |-  ( ( ph /\ Y e. ( A .no C ) ) -> ( Y e. ( A .no C ) <-> E. z e. A E. w e. C ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) )
14 1 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> A e. On )
15 2 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> B e. On )
16 14 15 nmulcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( A .no B ) e. On )
17 11 adantr 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> Y e. On )
18 simprll 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> z e. A )
19 14 18 onelond 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> z e. On )
20 3 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> C e. On )
21 simprlr 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> w e. C )
22 20 21 onelond 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> w e. On )
23 19 22 nmulcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no w ) e. On )
24 16 17 23 naddassd 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no B ) +no Y ) +no ( z .no w ) ) = ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) )
25 17 23 naddcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( Y +no ( z .no w ) ) e. On )
26 16 25 naddcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) e. On )
27 15 20 naddcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( B +no C ) e. On )
28 14 27 nmulcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( A .no ( B +no C ) ) e. On )
29 28 23 naddcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no C ) ) +no ( z .no w ) ) e. On )
30 simprr 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) )
31 19 20 nmulcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no C ) e. On )
32 14 22 nmulcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( A .no w ) e. On )
33 31 32 naddcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( z .no C ) +no ( A .no w ) ) e. On )
34 naddss2 
 |-  ( ( ( Y +no ( z .no w ) ) e. On /\ ( ( z .no C ) +no ( A .no w ) ) e. On /\ ( A .no B ) e. On ) -> ( ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) <-> ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) C_ ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) ) )
35 25 33 16 34 syl3anc 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) <-> ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) C_ ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) ) )
36 30 35 mpbid 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) C_ ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) )
37 oveq2 
 |-  ( f = w -> ( B +no f ) = ( B +no w ) )
38 37 oveq2d 
 |-  ( f = w -> ( A .no ( B +no f ) ) = ( A .no ( B +no w ) ) )
39 oveq2 
 |-  ( f = w -> ( A .no f ) = ( A .no w ) )
40 39 oveq2d 
 |-  ( f = w -> ( ( A .no B ) +no ( A .no f ) ) = ( ( A .no B ) +no ( A .no w ) ) )
41 38 40 eqeq12d 
 |-  ( f = w -> ( ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) <-> ( A .no ( B +no w ) ) = ( ( A .no B ) +no ( A .no w ) ) ) )
42 5 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) )
43 41 42 21 rspcdva 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( A .no ( B +no w ) ) = ( ( A .no B ) +no ( A .no w ) ) )
44 43 oveq1d 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no w ) ) +no ( z .no C ) ) = ( ( ( A .no B ) +no ( A .no w ) ) +no ( z .no C ) ) )
45 16 32 31 nadd32d 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no B ) +no ( A .no w ) ) +no ( z .no C ) ) = ( ( ( A .no B ) +no ( z .no C ) ) +no ( A .no w ) ) )
46 16 31 32 naddassd 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no B ) +no ( z .no C ) ) +no ( A .no w ) ) = ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) )
47 44 45 46 3eqtrrd 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) = ( ( A .no ( B +no w ) ) +no ( z .no C ) ) )
48 naddel2 
 |-  ( ( w e. On /\ C e. On /\ B e. On ) -> ( w e. C <-> ( B +no w ) e. ( B +no C ) ) )
49 22 20 15 48 syl3anc 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( w e. C <-> ( B +no w ) e. ( B +no C ) ) )
50 21 49 mpbid 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( B +no w ) e. ( B +no C ) )
51 nmuladdel 
 |-  ( ( ( A e. On /\ ( B +no C ) e. On ) /\ ( z e. A /\ ( B +no w ) e. ( B +no C ) ) ) -> ( ( z .no ( B +no C ) ) +no ( A .no ( B +no w ) ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no ( B +no w ) ) ) )
52 14 27 18 50 51 syl22anc 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( z .no ( B +no C ) ) +no ( A .no ( B +no w ) ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no ( B +no w ) ) ) )
53 15 22 naddcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( B +no w ) e. On )
54 14 53 nmulcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( A .no ( B +no w ) ) e. On )
55 19 15 nmulcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no B ) e. On )
56 54 31 55 naddassd 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) = ( ( A .no ( B +no w ) ) +no ( ( z .no C ) +no ( z .no B ) ) ) )
57 oveq1 
 |-  ( d = z -> ( d .no ( B +no C ) ) = ( z .no ( B +no C ) ) )
58 oveq1 
 |-  ( d = z -> ( d .no B ) = ( z .no B ) )
59 oveq1 
 |-  ( d = z -> ( d .no C ) = ( z .no C ) )
60 58 59 oveq12d 
 |-  ( d = z -> ( ( d .no B ) +no ( d .no C ) ) = ( ( z .no B ) +no ( z .no C ) ) )
61 57 60 eqeq12d 
 |-  ( d = z -> ( ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> ( z .no ( B +no C ) ) = ( ( z .no B ) +no ( z .no C ) ) ) )
62 4 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) )
63 61 62 18 rspcdva 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no ( B +no C ) ) = ( ( z .no B ) +no ( z .no C ) ) )
64 55 31 naddcomd 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( z .no B ) +no ( z .no C ) ) = ( ( z .no C ) +no ( z .no B ) ) )
65 63 64 eqtrd 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no ( B +no C ) ) = ( ( z .no C ) +no ( z .no B ) ) )
66 65 oveq2d 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no w ) ) +no ( z .no ( B +no C ) ) ) = ( ( A .no ( B +no w ) ) +no ( ( z .no C ) +no ( z .no B ) ) ) )
67 56 66 eqtr4d 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) = ( ( A .no ( B +no w ) ) +no ( z .no ( B +no C ) ) ) )
68 19 27 nmulcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no ( B +no C ) ) e. On )
69 54 68 naddcomd 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no w ) ) +no ( z .no ( B +no C ) ) ) = ( ( z .no ( B +no C ) ) +no ( A .no ( B +no w ) ) ) )
70 67 69 eqtrd 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) = ( ( z .no ( B +no C ) ) +no ( A .no ( B +no w ) ) ) )
71 28 23 55 naddassd 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no C ) ) +no ( z .no w ) ) +no ( z .no B ) ) = ( ( A .no ( B +no C ) ) +no ( ( z .no w ) +no ( z .no B ) ) ) )
72 23 55 naddcomd 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( z .no w ) +no ( z .no B ) ) = ( ( z .no B ) +no ( z .no w ) ) )
73 oveq1 
 |-  ( d = z -> ( d .no ( B +no f ) ) = ( z .no ( B +no f ) ) )
74 oveq1 
 |-  ( d = z -> ( d .no f ) = ( z .no f ) )
75 58 74 oveq12d 
 |-  ( d = z -> ( ( d .no B ) +no ( d .no f ) ) = ( ( z .no B ) +no ( z .no f ) ) )
76 73 75 eqeq12d 
 |-  ( d = z -> ( ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) <-> ( z .no ( B +no f ) ) = ( ( z .no B ) +no ( z .no f ) ) ) )
77 37 oveq2d 
 |-  ( f = w -> ( z .no ( B +no f ) ) = ( z .no ( B +no w ) ) )
78 oveq2 
 |-  ( f = w -> ( z .no f ) = ( z .no w ) )
79 78 oveq2d 
 |-  ( f = w -> ( ( z .no B ) +no ( z .no f ) ) = ( ( z .no B ) +no ( z .no w ) ) )
80 77 79 eqeq12d 
 |-  ( f = w -> ( ( z .no ( B +no f ) ) = ( ( z .no B ) +no ( z .no f ) ) <-> ( z .no ( B +no w ) ) = ( ( z .no B ) +no ( z .no w ) ) ) )
81 6 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) )
82 76 80 81 18 21 rspc2dv 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no ( B +no w ) ) = ( ( z .no B ) +no ( z .no w ) ) )
83 72 82 eqtr4d 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( z .no w ) +no ( z .no B ) ) = ( z .no ( B +no w ) ) )
84 83 oveq2d 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no C ) ) +no ( ( z .no w ) +no ( z .no B ) ) ) = ( ( A .no ( B +no C ) ) +no ( z .no ( B +no w ) ) ) )
85 71 84 eqtrd 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no C ) ) +no ( z .no w ) ) +no ( z .no B ) ) = ( ( A .no ( B +no C ) ) +no ( z .no ( B +no w ) ) ) )
86 52 70 85 3eltr4d 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) e. ( ( ( A .no ( B +no C ) ) +no ( z .no w ) ) +no ( z .no B ) ) )
87 54 31 naddcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no w ) ) +no ( z .no C ) ) e. On )
88 naddel1 
 |-  ( ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) e. On /\ ( ( A .no ( B +no C ) ) +no ( z .no w ) ) e. On /\ ( z .no B ) e. On ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) <-> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) e. ( ( ( A .no ( B +no C ) ) +no ( z .no w ) ) +no ( z .no B ) ) ) )
89 87 29 55 88 syl3anc 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) <-> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) e. ( ( ( A .no ( B +no C ) ) +no ( z .no w ) ) +no ( z .no B ) ) ) )
90 86 89 mpbird 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no w ) ) +no ( z .no C ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) )
91 47 90 eqeltrd 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) )
92 26 29 36 91 ontr2d 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) )
93 24 92 eqeltrd 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no B ) +no Y ) +no ( z .no w ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) )
94 16 17 naddcld 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no Y ) e. On )
95 naddel1 
 |-  ( ( ( ( A .no B ) +no Y ) e. On /\ ( A .no ( B +no C ) ) e. On /\ ( z .no w ) e. On ) -> ( ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) <-> ( ( ( A .no B ) +no Y ) +no ( z .no w ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) ) )
96 94 28 23 95 syl3anc 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) <-> ( ( ( A .no B ) +no Y ) +no ( z .no w ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) ) )
97 93 96 mpbird 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) )
98 97 expr 
 |-  ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( z e. A /\ w e. C ) ) -> ( ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) ) )
99 98 rexlimdvva 
 |-  ( ( ph /\ Y e. ( A .no C ) ) -> ( E. z e. A E. w e. C ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) ) )
100 13 99 sylbid 
 |-  ( ( ph /\ Y e. ( A .no C ) ) -> ( Y e. ( A .no C ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) ) )
101 100 syldbl2 
 |-  ( ( ph /\ Y e. ( A .no C ) ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) )