Metamath Proof Explorer

Theorem naddasslem2

Description: Lemma for naddass . Expand out the expression for natural addition of three arguments. (Contributed by Scott Fenton, 20-Jan-2025)

Ref Expression
Assertion naddasslem2 
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no ( B +no C ) ) = |^| { x e. On | ( A. a e. A ( a +no ( B +no C ) ) e. x /\ A. b e. B ( A +no ( b +no C ) ) e. x /\ A. c e. C ( A +no ( B +no c ) ) e. x ) } )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> A e. On )
2 naddcl 
 |-  ( ( B e. On /\ C e. On ) -> ( B +no C ) e. On )
3 2 3adant1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( B +no C ) e. On )
4 intmin 
 |-  ( A e. On -> |^| { a e. On | A C_ a } = A )
5 4 eqcomd 
 |-  ( A e. On -> A = |^| { a e. On | A C_ a } )
6 5 3ad2ant1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> A = |^| { a e. On | A C_ a } )
7 naddov3 
 |-  ( ( B e. On /\ C e. On ) -> ( B +no C ) = |^| { p e. On | ( ( +no " ( { B } X. C ) ) u. ( +no " ( B X. { C } ) ) ) C_ p } )
8 7 3adant1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( B +no C ) = |^| { p e. On | ( ( +no " ( { B } X. C ) ) u. ( +no " ( B X. { C } ) ) ) C_ p } )
9 1 3 6 8 naddunif 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no ( B +no C ) ) = |^| { x e. On | ( ( +no " ( A X. { ( B +no C ) } ) ) u. ( +no " ( { A } X. ( ( +no " ( { B } X. C ) ) u. ( +no " ( B X. { C } ) ) ) ) ) ) C_ x } )
10 3anass 
 |-  ( ( ( +no " ( A X. { ( B +no C ) } ) ) C_ x /\ ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) C_ x /\ ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) C_ x ) <-> ( ( +no " ( A X. { ( B +no C ) } ) ) C_ x /\ ( ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) C_ x /\ ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) C_ x ) ) )
11 unss 
 |-  ( ( ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) C_ x /\ ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) C_ x ) <-> ( ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) u. ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) ) C_ x )
12 ancom 
 |-  ( ( ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) C_ x /\ ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) C_ x ) <-> ( ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) C_ x /\ ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) C_ x ) )
13 xpundi 
 |-  ( { A } X. ( ( +no " ( { B } X. C ) ) u. ( +no " ( B X. { C } ) ) ) ) = ( ( { A } X. ( +no " ( { B } X. C ) ) ) u. ( { A } X. ( +no " ( B X. { C } ) ) ) )
14 13 imaeq2i 
 |-  ( +no " ( { A } X. ( ( +no " ( { B } X. C ) ) u. ( +no " ( B X. { C } ) ) ) ) ) = ( +no " ( ( { A } X. ( +no " ( { B } X. C ) ) ) u. ( { A } X. ( +no " ( B X. { C } ) ) ) ) )
15 imaundi 
 |-  ( +no " ( ( { A } X. ( +no " ( { B } X. C ) ) ) u. ( { A } X. ( +no " ( B X. { C } ) ) ) ) ) = ( ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) u. ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) )
16 14 15 eqtri 
 |-  ( +no " ( { A } X. ( ( +no " ( { B } X. C ) ) u. ( +no " ( B X. { C } ) ) ) ) ) = ( ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) u. ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) )
17 16 sseq1i 
 |-  ( ( +no " ( { A } X. ( ( +no " ( { B } X. C ) ) u. ( +no " ( B X. { C } ) ) ) ) ) C_ x <-> ( ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) u. ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) ) C_ x )
18 11 12 17 3bitr4i 
 |-  ( ( ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) C_ x /\ ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) C_ x ) <-> ( +no " ( { A } X. ( ( +no " ( { B } X. C ) ) u. ( +no " ( B X. { C } ) ) ) ) ) C_ x )
19 18 anbi2i 
 |-  ( ( ( +no " ( A X. { ( B +no C ) } ) ) C_ x /\ ( ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) C_ x /\ ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) C_ x ) ) <-> ( ( +no " ( A X. { ( B +no C ) } ) ) C_ x /\ ( +no " ( { A } X. ( ( +no " ( { B } X. C ) ) u. ( +no " ( B X. { C } ) ) ) ) ) C_ x ) )
20 unss 
 |-  ( ( ( +no " ( A X. { ( B +no C ) } ) ) C_ x /\ ( +no " ( { A } X. ( ( +no " ( { B } X. C ) ) u. ( +no " ( B X. { C } ) ) ) ) ) C_ x ) <-> ( ( +no " ( A X. { ( B +no C ) } ) ) u. ( +no " ( { A } X. ( ( +no " ( { B } X. C ) ) u. ( +no " ( B X. { C } ) ) ) ) ) ) C_ x )
21 10 19 20 3bitrri 
 |-  ( ( ( +no " ( A X. { ( B +no C ) } ) ) u. ( +no " ( { A } X. ( ( +no " ( { B } X. C ) ) u. ( +no " ( B X. { C } ) ) ) ) ) ) C_ x <-> ( ( +no " ( A X. { ( B +no C ) } ) ) C_ x /\ ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) C_ x /\ ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) C_ x ) )
22 naddfn 
 |-  +no Fn ( On X. On )
23 fnfun 
 |-  ( +no Fn ( On X. On ) -> Fun +no )
24 22 23 ax-mp 
 |-  Fun +no
25 onss 
 |-  ( A e. On -> A C_ On )
26 25 3ad2ant1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> A C_ On )
27 3 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( B +no C ) e. On )
28 27 snssd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> { ( B +no C ) } C_ On )
29 xpss12 
 |-  ( ( A C_ On /\ { ( B +no C ) } C_ On ) -> ( A X. { ( B +no C ) } ) C_ ( On X. On ) )
30 26 28 29 syl2an2r 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A X. { ( B +no C ) } ) C_ ( On X. On ) )
31 22 fndmi 
 |-  dom +no = ( On X. On )
32 30 31 sseqtrrdi 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A X. { ( B +no C ) } ) C_ dom +no )
33 funimassov 
 |-  ( ( Fun +no /\ ( A X. { ( B +no C ) } ) C_ dom +no ) -> ( ( +no " ( A X. { ( B +no C ) } ) ) C_ x <-> A. a e. A A. p e. { ( B +no C ) } ( a +no p ) e. x ) )
34 24 32 33 sylancr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( A X. { ( B +no C ) } ) ) C_ x <-> A. a e. A A. p e. { ( B +no C ) } ( a +no p ) e. x ) )
35 ovex 
 |-  ( B +no C ) e. _V
36 oveq2 
 |-  ( p = ( B +no C ) -> ( a +no p ) = ( a +no ( B +no C ) ) )
37 36 eleq1d 
 |-  ( p = ( B +no C ) -> ( ( a +no p ) e. x <-> ( a +no ( B +no C ) ) e. x ) )
38 35 37 ralsn 
 |-  ( A. p e. { ( B +no C ) } ( a +no p ) e. x <-> ( a +no ( B +no C ) ) e. x )
39 38 ralbii 
 |-  ( A. a e. A A. p e. { ( B +no C ) } ( a +no p ) e. x <-> A. a e. A ( a +no ( B +no C ) ) e. x )
40 34 39 bitrdi 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( A X. { ( B +no C ) } ) ) C_ x <-> A. a e. A ( a +no ( B +no C ) ) e. x ) )
41 simpl1 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> A e. On )
42 41 snssd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> { A } C_ On )
43 imassrn 
 |-  ( +no " ( B X. { C } ) ) C_ ran +no
44 naddf 
 |-  +no : ( On X. On ) --> On
45 frn 
 |-  ( +no : ( On X. On ) --> On -> ran +no C_ On )
46 44 45 ax-mp 
 |-  ran +no C_ On
47 43 46 sstri 
 |-  ( +no " ( B X. { C } ) ) C_ On
48 xpss12 
 |-  ( ( { A } C_ On /\ ( +no " ( B X. { C } ) ) C_ On ) -> ( { A } X. ( +no " ( B X. { C } ) ) ) C_ ( On X. On ) )
49 42 47 48 sylancl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( { A } X. ( +no " ( B X. { C } ) ) ) C_ ( On X. On ) )
50 49 31 sseqtrrdi 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( { A } X. ( +no " ( B X. { C } ) ) ) C_ dom +no )
51 funimassov 
 |-  ( ( Fun +no /\ ( { A } X. ( +no " ( B X. { C } ) ) ) C_ dom +no ) -> ( ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) C_ x <-> A. a e. { A } A. p e. ( +no " ( B X. { C } ) ) ( a +no p ) e. x ) )
52 24 50 51 sylancr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) C_ x <-> A. a e. { A } A. p e. ( +no " ( B X. { C } ) ) ( a +no p ) e. x ) )
53 oveq1 
 |-  ( a = A -> ( a +no p ) = ( A +no p ) )
54 53 eleq1d 
 |-  ( a = A -> ( ( a +no p ) e. x <-> ( A +no p ) e. x ) )
55 54 ralbidv 
 |-  ( a = A -> ( A. p e. ( +no " ( B X. { C } ) ) ( a +no p ) e. x <-> A. p e. ( +no " ( B X. { C } ) ) ( A +no p ) e. x ) )
56 55 ralsng 
 |-  ( A e. On -> ( A. a e. { A } A. p e. ( +no " ( B X. { C } ) ) ( a +no p ) e. x <-> A. p e. ( +no " ( B X. { C } ) ) ( A +no p ) e. x ) )
57 41 56 syl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. a e. { A } A. p e. ( +no " ( B X. { C } ) ) ( a +no p ) e. x <-> A. p e. ( +no " ( B X. { C } ) ) ( A +no p ) e. x ) )
58 onss 
 |-  ( B e. On -> B C_ On )
59 58 3ad2ant2 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> B C_ On )
60 simpl3 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> C e. On )
61 60 snssd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> { C } C_ On )
62 xpss12 
 |-  ( ( B C_ On /\ { C } C_ On ) -> ( B X. { C } ) C_ ( On X. On ) )
63 59 61 62 syl2an2r 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( B X. { C } ) C_ ( On X. On ) )
64 oveq2 
 |-  ( p = ( b +no c ) -> ( A +no p ) = ( A +no ( b +no c ) ) )
65 64 eleq1d 
 |-  ( p = ( b +no c ) -> ( ( A +no p ) e. x <-> ( A +no ( b +no c ) ) e. x ) )
66 65 imaeqalov 
 |-  ( ( +no Fn ( On X. On ) /\ ( B X. { C } ) C_ ( On X. On ) ) -> ( A. p e. ( +no " ( B X. { C } ) ) ( A +no p ) e. x <-> A. b e. B A. c e. { C } ( A +no ( b +no c ) ) e. x ) )
67 22 63 66 sylancr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( B X. { C } ) ) ( A +no p ) e. x <-> A. b e. B A. c e. { C } ( A +no ( b +no c ) ) e. x ) )
68 oveq2 
 |-  ( c = C -> ( b +no c ) = ( b +no C ) )
69 68 oveq2d 
 |-  ( c = C -> ( A +no ( b +no c ) ) = ( A +no ( b +no C ) ) )
70 69 eleq1d 
 |-  ( c = C -> ( ( A +no ( b +no c ) ) e. x <-> ( A +no ( b +no C ) ) e. x ) )
71 70 ralsng 
 |-  ( C e. On -> ( A. c e. { C } ( A +no ( b +no c ) ) e. x <-> ( A +no ( b +no C ) ) e. x ) )
72 60 71 syl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. c e. { C } ( A +no ( b +no c ) ) e. x <-> ( A +no ( b +no C ) ) e. x ) )
73 72 ralbidv 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. b e. B A. c e. { C } ( A +no ( b +no c ) ) e. x <-> A. b e. B ( A +no ( b +no C ) ) e. x ) )
74 67 73 bitrd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( B X. { C } ) ) ( A +no p ) e. x <-> A. b e. B ( A +no ( b +no C ) ) e. x ) )
75 52 57 74 3bitrd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) C_ x <-> A. b e. B ( A +no ( b +no C ) ) e. x ) )
76 imassrn 
 |-  ( +no " ( { B } X. C ) ) C_ ran +no
77 76 46 sstri 
 |-  ( +no " ( { B } X. C ) ) C_ On
78 xpss12 
 |-  ( ( { A } C_ On /\ ( +no " ( { B } X. C ) ) C_ On ) -> ( { A } X. ( +no " ( { B } X. C ) ) ) C_ ( On X. On ) )
79 42 77 78 sylancl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( { A } X. ( +no " ( { B } X. C ) ) ) C_ ( On X. On ) )
80 79 31 sseqtrrdi 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( { A } X. ( +no " ( { B } X. C ) ) ) C_ dom +no )
81 funimassov 
 |-  ( ( Fun +no /\ ( { A } X. ( +no " ( { B } X. C ) ) ) C_ dom +no ) -> ( ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) C_ x <-> A. a e. { A } A. p e. ( +no " ( { B } X. C ) ) ( a +no p ) e. x ) )
82 24 80 81 sylancr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) C_ x <-> A. a e. { A } A. p e. ( +no " ( { B } X. C ) ) ( a +no p ) e. x ) )
83 54 ralbidv 
 |-  ( a = A -> ( A. p e. ( +no " ( { B } X. C ) ) ( a +no p ) e. x <-> A. p e. ( +no " ( { B } X. C ) ) ( A +no p ) e. x ) )
84 83 ralsng 
 |-  ( A e. On -> ( A. a e. { A } A. p e. ( +no " ( { B } X. C ) ) ( a +no p ) e. x <-> A. p e. ( +no " ( { B } X. C ) ) ( A +no p ) e. x ) )
85 41 84 syl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. a e. { A } A. p e. ( +no " ( { B } X. C ) ) ( a +no p ) e. x <-> A. p e. ( +no " ( { B } X. C ) ) ( A +no p ) e. x ) )
86 simpl2 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> B e. On )
87 86 snssd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> { B } C_ On )
88 onss 
 |-  ( C e. On -> C C_ On )
89 88 3ad2ant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> C C_ On )
90 89 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> C C_ On )
91 xpss12 
 |-  ( ( { B } C_ On /\ C C_ On ) -> ( { B } X. C ) C_ ( On X. On ) )
92 87 90 91 syl2anc 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( { B } X. C ) C_ ( On X. On ) )
93 65 imaeqalov 
 |-  ( ( +no Fn ( On X. On ) /\ ( { B } X. C ) C_ ( On X. On ) ) -> ( A. p e. ( +no " ( { B } X. C ) ) ( A +no p ) e. x <-> A. b e. { B } A. c e. C ( A +no ( b +no c ) ) e. x ) )
94 22 92 93 sylancr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( { B } X. C ) ) ( A +no p ) e. x <-> A. b e. { B } A. c e. C ( A +no ( b +no c ) ) e. x ) )
95 oveq1 
 |-  ( b = B -> ( b +no c ) = ( B +no c ) )
96 95 oveq2d 
 |-  ( b = B -> ( A +no ( b +no c ) ) = ( A +no ( B +no c ) ) )
97 96 eleq1d 
 |-  ( b = B -> ( ( A +no ( b +no c ) ) e. x <-> ( A +no ( B +no c ) ) e. x ) )
98 97 ralbidv 
 |-  ( b = B -> ( A. c e. C ( A +no ( b +no c ) ) e. x <-> A. c e. C ( A +no ( B +no c ) ) e. x ) )
99 98 ralsng 
 |-  ( B e. On -> ( A. b e. { B } A. c e. C ( A +no ( b +no c ) ) e. x <-> A. c e. C ( A +no ( B +no c ) ) e. x ) )
100 86 99 syl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. b e. { B } A. c e. C ( A +no ( b +no c ) ) e. x <-> A. c e. C ( A +no ( B +no c ) ) e. x ) )
101 94 100 bitrd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( { B } X. C ) ) ( A +no p ) e. x <-> A. c e. C ( A +no ( B +no c ) ) e. x ) )
102 82 85 101 3bitrd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) C_ x <-> A. c e. C ( A +no ( B +no c ) ) e. x ) )
103 40 75 102 3anbi123d 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( ( +no " ( A X. { ( B +no C ) } ) ) C_ x /\ ( +no " ( { A } X. ( +no " ( B X. { C } ) ) ) ) C_ x /\ ( +no " ( { A } X. ( +no " ( { B } X. C ) ) ) ) C_ x ) <-> ( A. a e. A ( a +no ( B +no C ) ) e. x /\ A. b e. B ( A +no ( b +no C ) ) e. x /\ A. c e. C ( A +no ( B +no c ) ) e. x ) ) )
104 21 103 bitrid 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( ( +no " ( A X. { ( B +no C ) } ) ) u. ( +no " ( { A } X. ( ( +no " ( { B } X. C ) ) u. ( +no " ( B X. { C } ) ) ) ) ) ) C_ x <-> ( A. a e. A ( a +no ( B +no C ) ) e. x /\ A. b e. B ( A +no ( b +no C ) ) e. x /\ A. c e. C ( A +no ( B +no c ) ) e. x ) ) )
105 104 rabbidva 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> { x e. On | ( ( +no " ( A X. { ( B +no C ) } ) ) u. ( +no " ( { A } X. ( ( +no " ( { B } X. C ) ) u. ( +no " ( B X. { C } ) ) ) ) ) ) C_ x } = { x e. On | ( A. a e. A ( a +no ( B +no C ) ) e. x /\ A. b e. B ( A +no ( b +no C ) ) e. x /\ A. c e. C ( A +no ( B +no c ) ) e. x ) } )
106 105 inteqd 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> |^| { x e. On | ( ( +no " ( A X. { ( B +no C ) } ) ) u. ( +no " ( { A } X. ( ( +no " ( { B } X. C ) ) u. ( +no " ( B X. { C } ) ) ) ) ) ) C_ x } = |^| { x e. On | ( A. a e. A ( a +no ( B +no C ) ) e. x /\ A. b e. B ( A +no ( b +no C ) ) e. x /\ A. c e. C ( A +no ( B +no c ) ) e. x ) } )
107 9 106 eqtrd 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no ( B +no C ) ) = |^| { x e. On | ( A. a e. A ( a +no ( B +no C ) ) e. x /\ A. b e. B ( A +no ( b +no C ) ) e. x /\ A. c e. C ( A +no ( B +no c ) ) e. x ) } )