Metamath Proof Explorer

Theorem nadddilem4

Description: Lemma for nadddi . Prove the forward implication. (Contributed by Scott Fenton, 3-Aug-2026)

Ref Expression
Hypotheses nadddilem4.1 
|- ( ph -> A e. On )
nadddilem4.2 
|- ( ph -> B e. On )
nadddilem4.3 
|- ( ph -> C e. On )
nadddilem4.4 
|- ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) )
nadddilem4.5 
|- ( ph -> A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) )
nadddilem4.6 
|- ( ph -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) )
nadddilem4.7 
|- ( ph -> A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) )
nadddilem4.8 
|- ( ph -> A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) )
Assertion nadddilem4 
|- ( ph -> ( A .no ( B +no C ) ) C_ ( ( A .no B ) +no ( A .no C ) ) )

Proof

Step Hyp Ref Expression
1 nadddilem4.1 
 |-  ( ph -> A e. On )
2 nadddilem4.2 
 |-  ( ph -> B e. On )
3 nadddilem4.3 
 |-  ( ph -> C e. On )
4 nadddilem4.4 
 |-  ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) )
5 nadddilem4.5 
 |-  ( ph -> A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) )
6 nadddilem4.6 
 |-  ( ph -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) )
7 nadddilem4.7 
 |-  ( ph -> A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) )
8 nadddilem4.8 
 |-  ( ph -> A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) )
9 simprr 
 |-  ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> y e. ( B +no C ) )
10 2 3 naddcld 
 |-  ( ph -> ( B +no C ) e. On )
11 10 adantr 
 |-  ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( B +no C ) e. On )
12 11 9 onelond 
 |-  ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> y e. On )
13 2 adantr 
 |-  ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> B e. On )
14 3 adantr 
 |-  ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> C e. On )
15 ltnadd 
 |-  ( ( y e. On /\ B e. On /\ C e. On ) -> ( y e. ( B +no C ) <-> ( E. z e. B y C_ ( z +no C ) \/ E. w e. C y C_ ( B +no w ) ) ) )
16 12 13 14 15 syl3anc 
 |-  ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( y e. ( B +no C ) <-> ( E. z e. B y C_ ( z +no C ) \/ E. w e. C y C_ ( B +no w ) ) ) )
17 1 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> A e. On )
18 2 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> B e. On )
19 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> C e. On )
20 simplrl 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> x e. A )
21 simplrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> y e. ( B +no C ) )
22 simprl 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> z e. B )
23 simprr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> y C_ ( z +no C ) )
24 4 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) )
25 5 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) )
26 7 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) )
27 17 18 19 20 21 22 23 24 25 26 nadddilem3 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) )
28 27 rexlimdvaa 
 |-  ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( E. z e. B y C_ ( z +no C ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) )
29 1 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> A e. On )
30 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> C e. On )
31 2 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> B e. On )
32 simplrl 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> x e. A )
33 simplrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> y e. ( B +no C ) )
34 31 30 naddcomd 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( B +no C ) = ( C +no B ) )
35 33 34 eleqtrd 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> y e. ( C +no B ) )
36 simprl 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> w e. C )
37 simprr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> y C_ ( B +no w ) )
38 30 36 onelond 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> w e. On )
39 31 38 naddcomd 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( B +no w ) = ( w +no B ) )
40 37 39 sseqtrd 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> y C_ ( w +no B ) )
41 oveq1 
 |-  ( d = p -> ( d .no ( B +no C ) ) = ( p .no ( B +no C ) ) )
42 oveq1 
 |-  ( d = p -> ( d .no B ) = ( p .no B ) )
43 oveq1 
 |-  ( d = p -> ( d .no C ) = ( p .no C ) )
44 42 43 oveq12d 
 |-  ( d = p -> ( ( d .no B ) +no ( d .no C ) ) = ( ( p .no B ) +no ( p .no C ) ) )
45 41 44 eqeq12d 
 |-  ( d = p -> ( ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) ) )
46 45 cbvralvw 
 |-  ( A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> A. p e. A ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) )
47 2 3 naddcomd 
 |-  ( ph -> ( B +no C ) = ( C +no B ) )
48 47 adantr 
 |-  ( ( ph /\ p e. A ) -> ( B +no C ) = ( C +no B ) )
49 48 oveq2d 
 |-  ( ( ph /\ p e. A ) -> ( p .no ( B +no C ) ) = ( p .no ( C +no B ) ) )
50 1 adantr 
 |-  ( ( ph /\ p e. A ) -> A e. On )
51 simpr 
 |-  ( ( ph /\ p e. A ) -> p e. A )
52 50 51 onelond 
 |-  ( ( ph /\ p e. A ) -> p e. On )
53 2 adantr 
 |-  ( ( ph /\ p e. A ) -> B e. On )
54 52 53 nmulcld 
 |-  ( ( ph /\ p e. A ) -> ( p .no B ) e. On )
55 3 adantr 
 |-  ( ( ph /\ p e. A ) -> C e. On )
56 52 55 nmulcld 
 |-  ( ( ph /\ p e. A ) -> ( p .no C ) e. On )
57 54 56 naddcomd 
 |-  ( ( ph /\ p e. A ) -> ( ( p .no B ) +no ( p .no C ) ) = ( ( p .no C ) +no ( p .no B ) ) )
58 49 57 eqeq12d 
 |-  ( ( ph /\ p e. A ) -> ( ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) <-> ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) )
59 58 ralbidva 
 |-  ( ph -> ( A. p e. A ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) <-> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) )
60 46 59 bitrid 
 |-  ( ph -> ( A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) )
61 4 60 mpbid 
 |-  ( ph -> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) )
62 61 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) )
63 oveq2 
 |-  ( f = q -> ( B +no f ) = ( B +no q ) )
64 63 oveq2d 
 |-  ( f = q -> ( A .no ( B +no f ) ) = ( A .no ( B +no q ) ) )
65 oveq2 
 |-  ( f = q -> ( A .no f ) = ( A .no q ) )
66 65 oveq2d 
 |-  ( f = q -> ( ( A .no B ) +no ( A .no f ) ) = ( ( A .no B ) +no ( A .no q ) ) )
67 64 66 eqeq12d 
 |-  ( f = q -> ( ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) <-> ( A .no ( B +no q ) ) = ( ( A .no B ) +no ( A .no q ) ) ) )
68 67 cbvralvw 
 |-  ( A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) <-> A. q e. C ( A .no ( B +no q ) ) = ( ( A .no B ) +no ( A .no q ) ) )
69 2 adantr 
 |-  ( ( ph /\ q e. C ) -> B e. On )
70 3 adantr 
 |-  ( ( ph /\ q e. C ) -> C e. On )
71 simpr 
 |-  ( ( ph /\ q e. C ) -> q e. C )
72 70 71 onelond 
 |-  ( ( ph /\ q e. C ) -> q e. On )
73 69 72 naddcomd 
 |-  ( ( ph /\ q e. C ) -> ( B +no q ) = ( q +no B ) )
74 73 oveq2d 
 |-  ( ( ph /\ q e. C ) -> ( A .no ( B +no q ) ) = ( A .no ( q +no B ) ) )
75 1 2 nmulcld 
 |-  ( ph -> ( A .no B ) e. On )
76 75 adantr 
 |-  ( ( ph /\ q e. C ) -> ( A .no B ) e. On )
77 1 adantr 
 |-  ( ( ph /\ q e. C ) -> A e. On )
78 77 72 nmulcld 
 |-  ( ( ph /\ q e. C ) -> ( A .no q ) e. On )
79 76 78 naddcomd 
 |-  ( ( ph /\ q e. C ) -> ( ( A .no B ) +no ( A .no q ) ) = ( ( A .no q ) +no ( A .no B ) ) )
80 74 79 eqeq12d 
 |-  ( ( ph /\ q e. C ) -> ( ( A .no ( B +no q ) ) = ( ( A .no B ) +no ( A .no q ) ) <-> ( A .no ( q +no B ) ) = ( ( A .no q ) +no ( A .no B ) ) ) )
81 80 ralbidva 
 |-  ( ph -> ( A. q e. C ( A .no ( B +no q ) ) = ( ( A .no B ) +no ( A .no q ) ) <-> A. q e. C ( A .no ( q +no B ) ) = ( ( A .no q ) +no ( A .no B ) ) ) )
82 68 81 bitrid 
 |-  ( ph -> ( A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) <-> A. q e. C ( A .no ( q +no B ) ) = ( ( A .no q ) +no ( A .no B ) ) ) )
83 6 82 mpbid 
 |-  ( ph -> A. q e. C ( A .no ( q +no B ) ) = ( ( A .no q ) +no ( A .no B ) ) )
84 83 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> A. q e. C ( A .no ( q +no B ) ) = ( ( A .no q ) +no ( A .no B ) ) )
85 oveq1 
 |-  ( d = p -> ( d .no ( B +no f ) ) = ( p .no ( B +no f ) ) )
86 oveq1 
 |-  ( d = p -> ( d .no f ) = ( p .no f ) )
87 42 86 oveq12d 
 |-  ( d = p -> ( ( d .no B ) +no ( d .no f ) ) = ( ( p .no B ) +no ( p .no f ) ) )
88 85 87 eqeq12d 
 |-  ( d = p -> ( ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) <-> ( p .no ( B +no f ) ) = ( ( p .no B ) +no ( p .no f ) ) ) )
89 63 oveq2d 
 |-  ( f = q -> ( p .no ( B +no f ) ) = ( p .no ( B +no q ) ) )
90 oveq2 
 |-  ( f = q -> ( p .no f ) = ( p .no q ) )
91 90 oveq2d 
 |-  ( f = q -> ( ( p .no B ) +no ( p .no f ) ) = ( ( p .no B ) +no ( p .no q ) ) )
92 89 91 eqeq12d 
 |-  ( f = q -> ( ( p .no ( B +no f ) ) = ( ( p .no B ) +no ( p .no f ) ) <-> ( p .no ( B +no q ) ) = ( ( p .no B ) +no ( p .no q ) ) ) )
93 88 92 cbvral2vw 
 |-  ( A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) <-> A. p e. A A. q e. C ( p .no ( B +no q ) ) = ( ( p .no B ) +no ( p .no q ) ) )
94 73 adantrl 
 |-  ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( B +no q ) = ( q +no B ) )
95 94 oveq2d 
 |-  ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( p .no ( B +no q ) ) = ( p .no ( q +no B ) ) )
96 54 adantrr 
 |-  ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( p .no B ) e. On )
97 52 adantrr 
 |-  ( ( ph /\ ( p e. A /\ q e. C ) ) -> p e. On )
98 72 adantrl 
 |-  ( ( ph /\ ( p e. A /\ q e. C ) ) -> q e. On )
99 97 98 nmulcld 
 |-  ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( p .no q ) e. On )
100 96 99 naddcomd 
 |-  ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( ( p .no B ) +no ( p .no q ) ) = ( ( p .no q ) +no ( p .no B ) ) )
101 95 100 eqeq12d 
 |-  ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( ( p .no ( B +no q ) ) = ( ( p .no B ) +no ( p .no q ) ) <-> ( p .no ( q +no B ) ) = ( ( p .no q ) +no ( p .no B ) ) ) )
102 101 2ralbidva 
 |-  ( ph -> ( A. p e. A A. q e. C ( p .no ( B +no q ) ) = ( ( p .no B ) +no ( p .no q ) ) <-> A. p e. A A. q e. C ( p .no ( q +no B ) ) = ( ( p .no q ) +no ( p .no B ) ) ) )
103 93 102 bitrid 
 |-  ( ph -> ( A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) <-> A. p e. A A. q e. C ( p .no ( q +no B ) ) = ( ( p .no q ) +no ( p .no B ) ) ) )
104 8 103 mpbid 
 |-  ( ph -> A. p e. A A. q e. C ( p .no ( q +no B ) ) = ( ( p .no q ) +no ( p .no B ) ) )
105 104 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> A. p e. A A. q e. C ( p .no ( q +no B ) ) = ( ( p .no q ) +no ( p .no B ) ) )
106 29 30 31 32 35 36 40 62 84 105 nadddilem3 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( ( x .no ( C +no B ) ) +no ( A .no y ) ) e. ( ( ( A .no C ) +no ( A .no B ) ) +no ( x .no y ) ) )
107 34 oveq2d 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( x .no ( B +no C ) ) = ( x .no ( C +no B ) ) )
108 107 oveq1d 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) = ( ( x .no ( C +no B ) ) +no ( A .no y ) ) )
109 75 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( A .no B ) e. On )
110 1 3 nmulcld 
 |-  ( ph -> ( A .no C ) e. On )
111 110 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( A .no C ) e. On )
112 109 111 naddcomd 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( ( A .no B ) +no ( A .no C ) ) = ( ( A .no C ) +no ( A .no B ) ) )
113 112 oveq1d 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) = ( ( ( A .no C ) +no ( A .no B ) ) +no ( x .no y ) ) )
114 106 108 113 3eltr4d 
 |-  ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) )
115 114 rexlimdvaa 
 |-  ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( E. w e. C y C_ ( B +no w ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) )
116 28 115 jaod 
 |-  ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( ( E. z e. B y C_ ( z +no C ) \/ E. w e. C y C_ ( B +no w ) ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) )
117 16 116 sylbid 
 |-  ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( y e. ( B +no C ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) )
118 9 117 mpd 
 |-  ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) )
119 118 ralrimivva 
 |-  ( ph -> A. x e. A A. y e. ( B +no C ) ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) )
120 75 110 naddcld 
 |-  ( ph -> ( ( A .no B ) +no ( A .no C ) ) e. On )
121 nmulle 
 |-  ( ( A e. On /\ ( B +no C ) e. On /\ ( ( A .no B ) +no ( A .no C ) ) e. On ) -> ( ( A .no ( B +no C ) ) C_ ( ( A .no B ) +no ( A .no C ) ) <-> A. x e. A A. y e. ( B +no C ) ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) )
122 1 10 120 121 syl3anc 
 |-  ( ph -> ( ( A .no ( B +no C ) ) C_ ( ( A .no B ) +no ( A .no C ) ) <-> A. x e. A A. y e. ( B +no C ) ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) )
123 119 122 mpbird 
 |-  ( ph -> ( A .no ( B +no C ) ) C_ ( ( A .no B ) +no ( A .no C ) ) )